Dedication

Preface

The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that a certain kind of formal structure may be read in two ways: either as a proposition in logic or as a type in computing. Further, a related structure may be read as either the proof of the proposition or as a programme of the corresponding type. Further still, simplification of proofs corresponds to evaluation of programs.

Accordingly, the title of this book also has two readings. It may be parsed as “(Programming Language) Foundations in Agda” or “Programming (Language Foundations) in Agda” — the specifications we will write in the proof assistant Agda both describe programming languages and are themselves programmes.

The book is aimed at students in the last year of an undergraduate honours programme or the first year of a master or doctorate degree. It aims to teach the fundamentals of operational semantics of programming languages, with simply-typed lambda calculus as the central example. The textbook is written as a literate script in Agda. The hope is that using a proof assistant will make the development more concrete and accessible to students, and give them rapid feedback to find and correct misapprehensions.

The book is broken into two parts. The first part, Logical Foundations, develops the needed formalisms. The second part, Programming Language Foundations, introduces basic methods of operational semantics.

Personal remarks

Since 2013, I have taught a course on Types and Semantics for Programming Languages to fourth-year undergraduates and masters students at the University of Edinburgh. An earlier version of that course was based on Benjamin Pierce’s excellent TAPL. My version was based of Pierce’s subsequent textbook, Software Foundations, written in collaboration with others and based on Coq. I am convinced of Pierce’s claim that basing a course around a proof assistant aids learning, as summarised in his ICFP Keynote, Lambda, The Ultimate TA.

However, after five years of experience, I have come to the conclusion that Coq is not the best vehicle. Too much of the course needs to focus on learning tactics for proof derivation, to the cost of learning the fundamentals of programming language theory. Every concept has to be learned twice: e.g., both the product data type, and the corresponding tactics for introduction and elimination of conjunctions. The rules Coq applies to generate induction hypotheses can sometimes seem mysterious. While the notation construct permits pleasingly flexible syntax, it can be confusing that the same concept must always be given two names, e.g., both subst N x M and N [x := M]. Names of tactics are sometimes short and sometimes long; naming conventions in the standard library can be wildly inconsistent. Propositions as types as a foundation of proof is present but hidden.

I found myself keen to recast the course in Agda. In Agda, there is no longer any need to learn about tactics: there is just dependently-typed programming, plain and simple. Introduction is always by a constructor, elimination is always by pattern matching. Induction is no longer a mysterious separate concept, but corresponds to the familiar notion of recursion. Mixfix syntax is flexible while using just one name for each concept, e.g., substitution is _[_:=_]. The standard library is not perfect, but there is a fair attempt at consistency. Propositions as types as a foundation of proof is on proud display.

Alas, there is no textbook for programming language theory in Agda. Stump’s Verified Functional Programming in Agda covers related ground, but focusses more on programming with dependent types than on the theory of programming languages.

The original goal was to simply adapt Software Foundations, maintaining the same text but transposing the code from Coq to Agda. But it quickly became clear to me that after five years in the classroom I had my own ideas about how to present the material. They say you should never write a book unless you cannot not write the book, and I soon found that this was a book I could not not write.

I am fortunate that my student, Wen Kokke, was keen to help. She guided me as a newbie to Agda and provided an infrastructure that is easy to use and produces pages that are a pleasure to view.

Most of the text was written during a sabbatical in the first half of 2018.

— Philip Wadler, Rio de Janeiro, January–June 2018

A word on the exercises

Exercises labelled “(recommended)” are the ones students are required to do in the class taught at Edinburgh from this textbook.

Exercises labelled “(stretch)” are there to provide an extra challenge. Few students do all of these, but most attempt at least a few.

Exercises labelled “(practice)” are included for those who want extra practice.

You may need to import library functions required for the solution.

Please do not post answers to the exercises in a public place.

There is a private repository of answers to selected questions on github. Please contact Philip Wadler if you would like to access it.

Getting Started

Getting Started for Readers

You can read PLFA online without installing anything. However, if you wish to interact with the code or complete the exercises, you need several things:

• On macOS: The XCode Command Line Tools
• Git
• GHC and Cabal
• Agda
• Agda standard library
• PLFA

PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems.

There are several versions of Agda and its standard library online. If you are using a package manager, like Homebrew or Debian apt, the version of Agda available there may be out of date. Furthermore, Agda is under active development, so if you install the development version from the GitHub, you might find the developers have introduced changes which break the code here. Therefore, it’s important to have the specific versions of Agda and the standard library shown above.

On macOS: Install the XCode Command Line Tools

On macOS, you’ll need to install The XCode Command Line Tools. For most versions of macOS, you can install these by running the following command:

xcode-select --install

Install Git

You can check whether you have Git by running the following command:

git --version

If you do not have Git, see the Git downloads page.

Install GHC and Cabal

Agda is written in Haskell, so to install it we’ll need the Glorious Haskell Compiler (version 8.10.7 or 9.2.3) and its package manager Cabal. We recommend installing these using ghcup.

Install Agda

The easiest way to install Agda is using Cabal. PLFA uses Agda version 2.6.2.2. Run the following command:

cabal update
cabal install Agda-2.6.2.2

This step will take a long time and a lot of memory to complete.

If you have problems or for alternatives see the Agda installation instructions.

If you’d like, you can test to see if you’ve installed Agda correctly.

Install PLFA and the Agda standard library

We recommend installing PLFA from Github into your home directory, by running the following command:

git clone --depth 1 --recurse-submodules --shallow-submodules https://github.com/plfa/plfa.github.io plfa

PLFA ships with the required version of the Agda standard library, so if you cloned with the --recurse-submodules flag, you’ve already got it, in the standard-library directory!

Finally, we need to let Agda know where to find the Agda standard library and PLFA. Two configuration files are required, one which lists paths to the libraries and one which specifies which libraries to load by default.

On macOS and Unix, if PLFA is installed in your home directory and you have no existing library configuration files you wish to preserve, run the following commands:

mkdir -p ~/.agda
cp ~/plfa/data/dotagda/* ~/.agda

This provides access to both the Agda standard library and to PLFA as an Agda library.

Otherwise, you will need to edit the appropriate files. Both configuration files are located in the directory AGDA_DIR. On UNIX and macOS, AGDA_DIR defaults to ~/.agda. On Windows, AGDA_DIR usually defaults to %AppData%\agda, where %AppData% usually defaults to C:\Users\USERNAME\AppData\Roaming.

• If the AGDA_DIR directory does not already exist, create it.
• In AGDA_DIR, create a plain-text file called libraries containing AGDA_STDLIB/standard-library.agda-lib, where AGDA_STDLIB is the path to where the Agda standard library is located (e.g., ~/plfa/standard-library/). This lets Agda know that an Agda library called standard-library is available.
• In AGDA_DIR, create a plain-text file called defaults containing just the line standard-library.
• If you want to complete the exercises or to import modules from the book, you will also need to provide access to PLFA as an Agda library. To do so, let PLFA be the path to the root directory for PLFA. Add PLFA/src/plfa.agda-lib to AGDA_DIR/libraries and add plfa to AGDA_DIR/defaults, each on a line of their own.

More information about placing the standard libraries is available from the Library Management page of the Agda documentation.

Setting up an editor for Agda

Emacs

The recommended editor for Agda is Emacs. To install Emacs:

• On UNIX, the version of Emacs in your repository is probably fine as long as it is fairly recent. There are also links to the most recent release on the GNU Emacs downloads page.

• On MacOS, Aquamacs is probably the preferred version of Emacs, but GNU Emacs can also be installed via Homebrew or MacPorts. See the GNU Emacs downloads page for instructions.

• On Windows. See the GNU Emacs downloads page for instructions.

Make sure that you are able to open, edit, and save text files with your installation. The tour of Emacs page on the GNU Emacs site describes how to access the tutorial within your Emacs installation.

Agda ships with the editor support for Emacs built-in, so if you’ve installed Agda, all you have to do to configure Emacs is run:

agda-mode setup
agda-mode compile

If you are already an Emacs user and have customized your setup, you may want to note the configuration which the setup appends to your .emacs file, and integrate it with your own preferred setup.

Check if agda-mode was installed correctly

Open the nats.agda file you created earlier, and load and type-check the file by typing C-c C-l.

Auto-loading agda-mode in Emacs

Since version 2.6.0, Agda has had support for literate editing with Markdown, using the .lagda.md extension. One issue is that Emacs will default to Markdown editing mode for files with a .md suffix. In order to have agda-mode automatically loaded whenever you open a file ending with .agda or .lagda.md, add the following line to your Emacs configuration file:

;; auto-load agda-mode for .agda and .lagda.md
(setq auto-mode-alist
   (append
     '(("\\.agda\\'" . agda2-mode)
       ("\\.lagda.md\\'" . agda2-mode))
     auto-mode-alist))

If you already have settings which change your auto-mode-alist in your configuration, put these after the ones you already have or combine them if you are comfortable with Emacs Lisp. The configuration file for Emacs is normally located in HOME/.emacs or HOME/.emacs.d/init.el, but Aquamacs users might need to move their startup settings to the “Preferences.el” file in HOME/Library/Preferences/Aquamacs Emacs/Preferences. For Windows, see the GNU Emacs documentation for a description of where the Emacs configuration is located.

Optional: using the mononoki font with Emacs

Agda uses Unicode characters for many key symbols, and it is important that the font which you use to view and edit Agda programs shows these symbols correctly. The most important part is that the font you use has good Unicode support, so while we recommend mononoki, fonts such as Source Code Pro, DejaVu Sans Mono, and FreeMono are all good alternatives.

You can download and install mononoki directly from GitHub. For most systems, installing a font is merely a matter of clicking the downloaded .otf or .ttf file. If your package manager offers a package for mononoki, that might be easier. For instance, Homebrew on macOS offers the font-mononoki package in the cask-fonts cask, and APT on Debian offers the fonts-mononoki package. To configure Emacs to use mononoki as its default font, add the following to the end of your Emacs configuration file:

;; default to mononoki
(set-face-attribute 'default nil
                    :family "mononoki"
                    :height 120
                    :weight 'normal
                    :width  'normal)

Using agda-mode in Emacs

To load and type-check the file, use C-c C-l.

Agda is edited interactively, using “holes”, which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer using C-c C-l, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole:

• C-c C-c: case split (asks for variable name)
• C-c C-space: fill in hole
• C-c C-r: refine with constructor
• C-c C-a: automatically fill in hole
• C-c C-,: goal type and context
• C-c C-.: goal type, context, and inferred type

See the emacs-mode docs for more details.

If you want to see messages beside rather than below your Agda code, you can do the following:

• Open your Agda file, and load it using C-c C-l;
• type C-x 1 to get only your Agda file showing;
• type C-x 3 to split the window horizontally;
• move your cursor to the right-hand half of your frame;
• type C-x b and switch to the buffer called “Agda information”.

Now, error messages from Agda will appear next to your file, rather than squished beneath it.

Entering Unicode characters in Emacs with agda-mode

When you write Agda code, you will need to insert characters which are not found on standard keyboards. Emacs “agda-mode” makes it easier to do this by defining character translations: when you enter certain sequences of ordinary characters (the kind you find on any keyboard), Emacs will replace them in your Agda file with the corresponding special character.

For example, we can add a comment line to one of the .agda test files. Let’s say we want to add a comment line that reads:

{- I am excited to type ∀ and → and ≤ and ≡ !! -}

The first few characters are ordinary, so we would just type them as usual…

{- I am excited to type

But after that last space, we do not find ∀ on the keyboard. The code for this character is the four characters \all, so we type those four characters, and when we finish, Emacs will replace them with what we want…

{- I am excited to type ∀

We can continue with the codes for the other characters. Sometimes the characters will change as we type them, because a prefix of our character’s code is the code of another character. This happens with the arrow, whose code is \->. After typing \- we see…

{- I am excited to type ∀ and -

…because the code \- corresponds to a hyphen of a certain width. When we add the >, the - becomes →! The code for ≤ is \<=, and the code for ≡ is \==.

{- I am excited to type ∀ and → and ≤ and ≡

Finally the last few characters are ordinary again…

{- I am excited to type ∀ and → and ≤ and ≡ !! -}

If you’re having trouble typing the Unicode characters into Emacs, the end of each chapter should provide a list of the Unicode characters introduced in that chapter.

Emacs with agda-mode offers a number of useful commands, and two of them are especially useful when it comes to working with Unicode characters. For a full list of supported characters, use agda-input-show-translations with:

M-x agda-input-show-translations

All the supported characters in agda-mode are shown.

If you want to know how you input a specific Unicode character in agda file, move the cursor onto the character and type the following command:

M-x quail-show-key

You’ll see the key sequence of the character in mini buffer.

Spacemacs

Spacemacs is a “community-driven Emacs distribution” with native support for both Emacs and Vim editing styles. It comes with integration for agda-mode out of the box. All that is required is that you turn it on.

Visual Studio Code

Visual Studio Code is a free source code editor developed by Microsoft. There is a plugin for Agda support available on the Visual Studio Marketplace.

Atom

Atom is a free source code editor developed by GitHub. There is a plugin for Agda support available on the Atom package manager.

Naturals: Natural numbers

module plfa.part1.Naturals where

The night sky holds more stars than I can count, though fewer than five thousand are visible to the naked eye. The observable universe contains about seventy sextillion stars.

But the number of stars is finite, while natural numbers are infinite. Count all the stars, and you will still have as many natural numbers left over as you started with.

The naturals are an inductive datatype

Everyone is familiar with the natural numbers

0
1
2
3
...

and so on. We write ℕ for the type of natural numbers, and say that 0, 1, 2, 3, and so on are values of type ℕ, indicated by writing 0 : ℕ, 1 : ℕ, 2 : ℕ, 3 : ℕ, and so on.

The set of natural numbers is infinite, yet we can write down its definition in just a few lines. Here is the definition as a pair of inference rules:

--------
zero : ℕ

m : ℕ
---------
suc m : ℕ

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

Here ℕ is the name of the datatype we are defining, and zero and suc (short for successor) are the constructors of the datatype.

Both definitions above tell us the same two things:

• Base case: zero is a natural number.
• Inductive case: if m is a natural number, then suc m is also a natural number.

Further, these two rules give the only ways of creating natural numbers. Hence, the possible natural numbers are:

zero
suc zero
suc (suc zero)
suc (suc (suc zero))
...

We write 0 as shorthand for zero; and 1 is shorthand for suc zero, the successor of zero, that is, the natural that comes after zero; and 2 is shorthand for suc (suc zero), which is the same as suc 1, the successor of one; and 3 is shorthand for the successor of two; and so on.

Exercise seven (practice)

Write out 7 in longhand.

-- Your code goes here

You will need to give both a type signature and definition for the variable seven. Type C-c C-l in Emacs to instruct Agda to re-load.

Unpacking the inference rules

Let’s unpack the inference rules. Each inference rule consists of zero or more judgments written above a horizontal line, called the hypotheses, and a single judgment written below, called the conclusion. The first rule is the base case. It has no hypotheses, and the conclusion asserts that zero is a natural. The second rule is the inductive case. It has one hypothesis, which assumes that m is a natural, and the conclusion asserts that suc m is also a natural.

Unpacking the Agda definition

Let’s unpack the Agda definition. The keyword data tells us this is an inductive definition, that is, that we are defining a new datatype with constructors. The phrase

ℕ : Set

tells us that ℕ is the name of the new datatype, and that it is a Set, which is the way in Agda of saying that it is a type. The keyword where separates the declaration of the datatype from the declaration of its constructors. Each constructor is declared on a separate line, which is indented to indicate that it belongs to the corresponding data declaration. The lines

zero : ℕ
suc  : ℕ → ℕ

give signatures specifying the types of the constructors zero and suc. They tell us that zero is a natural number and that suc takes a natural number as an argument and returns a natural number.

You may have noticed that ℕ and → don’t appear on your keyboard. They are symbols in unicode. At the end of each chapter is a list of all unicode symbols introduced in the chapter, including instructions on how to type them in the Emacs text editor. Here type refers to typing with fingers as opposed to data types!

The story of creation

Let’s look again at the rules that define the natural numbers:

• Base case: zero is a natural number.
• Inductive case: if m is a natural number, then suc m is also a natural number.

Hold on! The second line defines natural numbers in terms of natural numbers. How can that possibly be allowed? Isn’t this as useless a definition as “Brexit means Brexit”?

In fact, it is possible to assign our definition a meaning without resorting to unpermitted circularities. Furthermore, we can do so while only working with finite sets and never referring to the infinite set of natural numbers.

We will think of it as a creation story. To start with, we know about no natural numbers at all:

-- In the beginning, there are no natural numbers.

Now, we apply the rules to all the natural numbers we know about. The base case tells us that zero is a natural number, so we add it to the set of known natural numbers. The inductive case tells us that if m is a natural number (on the day before today) then suc m is also a natural number (today). We didn’t know about any natural numbers before today, so the inductive case doesn’t apply:

-- On the first day, there is one natural number.
zero : ℕ

Then we repeat the process. On the next day we know about all the numbers from the day before, plus any numbers added by the rules. The base case tells us that zero is a natural number, but we already knew that. But now the inductive case tells us that since zero was a natural number yesterday, then suc zero is a natural number today:

-- On the second day, there are two natural numbers.
zero : ℕ
suc zero : ℕ

And we repeat the process again. Now the inductive case tells us that since zero and suc zero are both natural numbers, then suc zero and suc (suc zero) are natural numbers. We already knew about the first of these, but the second is new:

-- On the third day, there are three natural numbers.
zero : ℕ
suc zero : ℕ
suc (suc zero) : ℕ

You’ve got the hang of it by now:

-- On the fourth day, there are four natural numbers.
zero : ℕ
suc zero : ℕ
suc (suc zero) : ℕ
suc (suc (suc zero)) : ℕ

The process continues. On the n’th day there will be n distinct natural numbers. Every natural number will appear on some given day. In particular, the number n first appears on day n+1. And we never actually define the set of numbers in terms of itself. Instead, we define the set of numbers on day n+1 in terms of the set of numbers on day n.

A process like this one is called inductive. We start with nothing, and build up a potentially infinite set by applying rules that convert one finite set into another finite set.

The rule defining zero is called a base case, because it introduces a natural number even when we know no other natural numbers. The rule defining successor is called an inductive case, because it introduces more natural numbers once we already know some. Note the crucial role of the base case. If we only had inductive rules, then we would have no numbers in the beginning, and still no numbers on the second day, and on the third, and so on. An inductive definition lacking a base case is useless, as in the phrase “Brexit means Brexit”.

Philosophy and history

A philosopher might observe that our reference to the first day, second day, and so on, implicitly involves an understanding of natural numbers. In this sense, our definition might indeed be regarded as in some sense circular, but we need not let this disturb us. Everyone possesses a good informal understanding of the natural numbers, which we may take as a foundation for their formal description.

While the natural numbers have been understood for as long as people can count, the inductive definition of the natural numbers is relatively recent. It can be traced back to Richard Dedekind’s paper “Was sind und was sollen die Zahlen?” (What are and what should be the numbers?), published in 1888, and Giuseppe Peano’s book “Arithmetices principia, nova methodo exposita” (The principles of arithmetic presented by a new method), published the following year.

A pragma

In Agda, any text following -- or enclosed between {- and -} is considered a comment. Comments have no effect on the code, with the exception of one special kind of comment, called a pragma, which is enclosed between {-# and #-}.

{-# BUILTIN NATURAL ℕ #-}

tells Agda that ℕ corresponds to the natural numbers, and hence one is permitted to type 0 as shorthand for zero, 1 as shorthand for suc zero, 2 as shorthand for suc (suc zero), and so on. The pragma must be given a previously declared type (in this case ℕ) with precisely two constructors, one with no arguments (in this case zero), and one with a single argument of the given type (in this case suc).

As well as enabling the above shorthand, the pragma also enables a more efficient internal representation of naturals using the Haskell type for arbitrary-precision integers. Representing the natural n with zero and suc requires space proportional to n, whereas representing it as an arbitrary-precision integer in Haskell only requires space proportional to the logarithm of n.

Imports

Shortly we will want to write some equations that hold between terms involving natural numbers. To support doing so, we import the definition of equality and notations for reasoning about it from the Agda standard library:

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

The first line brings the standard library module that defines equality into scope and gives it the name Eq. The second line opens that module, that is, adds all the names specified in the using clause into the current scope. In this case the names added are _≡_, the equality operator, and refl, the name for evidence that two terms are equal. The third line takes a module that specifies operators to support reasoning about equivalence, and adds all the names specified in the using clause into the current scope. In this case, the names added are begin_, _≡⟨⟩_, and _∎. We will see how these are used below. We take these as givens for now, but will see how they are defined in Chapter Equality.

Agda uses underbars to indicate where terms appear in infix or mixfix operators. Thus, _≡_ and _≡⟨⟩_ are infix (each operator is written between two terms), while begin_ is prefix (it is written before a term), and _∎ is postfix (it is written after a term).

Parentheses and semicolons are among the few characters that cannot appear in names, so we do not need extra spaces in the using list.

Operations on naturals are recursive functions

Now that we have the natural numbers, what can we do with them? For instance, can we define arithmetic operations such as addition and multiplication?

As a child I spent much time memorising tables of addition and multiplication. At first the rules seemed tricky and I would often make mistakes. It came as a shock to me to discover recursion, a simple technique by which every one of the infinite possible instances of addition and multiplication can be specified in just a couple of lines.

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

Let’s unpack this definition. Addition is an infix operator. It is written with underbars where the arguments go, hence its name is _+_. The first line is a signature specifying the type of the operator. The type ℕ → ℕ → ℕ, indicates that addition accepts two naturals and returns a natural. Infix notation is just a shorthand for application; the terms m + n and _+_ m n are equivalent.

The definition has a base case and an inductive case, corresponding to those for the natural numbers. The base case says that adding zero to a number, zero + n, returns that number, n. The inductive case says that adding the successor of a number to another number, (suc m) + n, returns the successor of adding the two numbers, suc (m + n). We say we use pattern matching when constructors appear on the left-hand side of an equation.

If we write zero as 0 and suc m as 1 + m, the definition turns into two familiar equations:

 0       + n  ≡  n
 (1 + m) + n  ≡  1 + (m + n)

The first follows because zero is an identity for addition, and the second because addition is associative. In its most general form, associativity is written

 (m + n) + p  ≡  m + (n + p)

meaning that the location of parentheses is irrelevant. We get the second equation from the third by taking m to be 1, n to be m, and p to be n. We write = for definitions, while we write ≡ for assertions that two already defined things are the same.

The definition is recursive, in that the last line defines addition in terms of addition. As with the inductive definition of the naturals, the apparent circularity is not a problem. It works because addition of larger numbers is defined in terms of addition of smaller numbers. Such a definition is called well founded.

_ :  +  ≡ 
_ =
  begin
     + 
  ≡⟨⟩    -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- inductive case
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩    -- inductive case
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩    -- base case
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩    -- is longhand for
    
  ∎

_ :  +  ≡ 
_ =
  begin
     + 
  ≡⟨⟩
    suc ( + )
  ≡⟨⟩
    suc (suc ( + ))
  ≡⟨⟩
    suc (suc )
  ≡⟨⟩
    
  ∎

The first line matches the inductive case by taking m = 1 and n = 3, the second line matches the inductive case by taking m = 0 and n = 3, and the third line matches the base case by taking n = 3.

Both derivations consist of a signature (written with a colon, :), giving a type, and a binding (written with an equal sign, =), giving a term of the given type. Here we use the dummy name _. The dummy name can be reused, and is convenient for examples. Names other than _ must be used only once in a module.

Here the type is 2 + 3 ≡ 5 and the term provides evidence for the corresponding equation, here written in tabular form as a chain of equations. The chain starts with begin and finishes with ∎ (pronounced “qed” or “tombstone”, the latter from its appearance), and consists of a series of terms separated by ≡⟨⟩.

_ :  +  ≡ 
_ = refl

Agda knows how to compute the value of 2 + 3, and so can immediately check it is the same as 5. A binary relation is said to be reflexive if every value relates to itself. Evidence that a value is equal to itself is written refl.

In the chains of equations, all Agda checks is that each term simplifies to the same value. If we jumble the equations, omit lines, or add extraneous lines it will still be accepted. It’s up to us to write the equations in an order that makes sense to the reader.

Here 2 + 3 ≡ 5 is a type, and the chains of equations (and also refl) are terms of the given type; alternatively, one can think of each term as evidence for the assertion 2 + 3 ≡ 5. This duality of interpretation—of a type as a proposition, and of a term as evidence—is central to how we formalise concepts in Agda, and will be a running theme throughout this book.

Note that when we use the word evidence it is nothing equivocal. It is not like testimony in a court which must be weighed to determine whether the witness is trustworthy. Rather, it is ironclad. The other word for evidence, which we will use interchangeably, is proof.

Exercise +-example (practice)

Compute 3 + 4, writing out your reasoning as a chain of equations, using the equations for +.

-- Your code goes here

Multiplication

_*_ : ℕ → ℕ → ℕ
zero    * n  =  zero
(suc m) * n  =  n + (m * n)

Computing m * n returns the sum of m copies of n.

Again, rewriting turns the definition into two familiar equations:

0       * n  ≡  0
(1 + m) * n  ≡  n + (m * n)

The first follows because zero times anything is zero, and the second follows because multiplication distributes over addition. In its most general form, distribution of multiplication over addition is written

(m + n) * p  ≡  (m * p) + (n * p)

We get the second equation from the third by taking m to be 1, n to be m, and p to be n, and then using the fact that one is an identity for multiplication, so 1 * n ≡ n.

Again, the definition is well founded in that multiplication of larger numbers is defined in terms of multiplication of smaller numbers.

_ =
  begin
     * 
  ≡⟨⟩    -- inductive case
     + ( * )
  ≡⟨⟩    -- inductive case
     + ( + ( * ))
  ≡⟨⟩    -- base case
     + ( + )
  ≡⟨⟩    -- simplify
    
  ∎

The first line matches the inductive case by taking m = 1 and n = 3, the second line matches the inductive case by taking m = 0 and n = 3, and the third line matches the base case by taking n = 3. Here we have omitted the signature declaring _ : 2 * 3 ≡ 6, since it can easily be inferred from the corresponding term.

Exercise *-example (practice)

Compute 3 * 4, writing out your reasoning as a chain of equations, using the equations for *. (You do not need to step through the evaluation of +.)

-- Your code goes here

Exercise _^_ (recommended)

Define exponentiation, which is given by the following equations:

m ^ 0        =  1
m ^ (1 + n)  =  m * (m ^ n)

Check that 3 ^ 4 is 81.

-- Your code goes here

Monus

We can also define subtraction. Since there are no negative natural numbers, if we subtract a larger number from a smaller number we will take the result to be zero. This adaption of subtraction to naturals is called monus (a twist on minus).

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

We can do a simple analysis to show that all the cases are covered.

• Consider the second argument.
  • If it is zero, then the first equation applies.
  • If it is suc n, then consider the first argument.
    • If it is zero, then the second equation applies.
    • If it is suc m, then the third equation applies.

Again, the recursive definition is well founded because monus on bigger numbers is defined in terms of monus on smaller numbers.

_ =
  begin
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
    
  ∎

_ =
  begin
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
    
  ∎

Exercise ∸-example₁ and ∸-example₂ (recommended)

Compute 5 ∸ 3 and 3 ∸ 5, writing out your reasoning as a chain of equations.

-- Your code goes here

Precedence

We often use precedence to avoid writing too many parentheses. Application binds more tightly than (or has precedence over) any operator, and so we may write suc m + n to mean (suc m) + n. As another example, we say that multiplication binds more tightly than addition, and so write n + m * n to mean n + (m * n). We also sometimes say that addition associates to the left, and so write m + n + p to mean (m + n) + p.

infixl   _+_  _∸_
infixl   _*_

This states operators _+_ and _∸_ have precedence level 6, and operator _*_ has precedence level 7. Addition and monus bind less tightly than multiplication because they have lower precedence. Writing infixl indicates that all three operators associate to the left. One can also write infixr to indicate that an operator associates to the right, or just infix to indicate that parentheses are always required to disambiguate.

Currying

We have chosen to represent a function of two arguments in terms of a function of the first argument that returns a function of the second argument. This trick goes by the name currying.

Agda, like other functional languages such as Haskell and ML, is designed to make currying easy to use. Function arrows associate to the right and application associates to the left

ℕ → ℕ → ℕ stands for ℕ → (ℕ → ℕ)

and

_+_ 2 3 stands for (_+_ 2) 3.

The term _+_ 2 by itself stands for the function that adds two to its argument, hence applying it to three yields five.

Currying is named for Haskell Curry, after whom the programming language Haskell is also named. Curry’s work dates to the 1930’s. When I first learned about currying, I was told it was misattributed, since the same idea was previously proposed by Moses Schönfinkel in the 1920’s. I was told a joke: “It should be called schönfinkeling, but currying is tastier”. Only later did I learn that the explanation of the misattribution was itself a misattribution. The idea actually appears in the Begriffsschrift of Gottlob Frege, published in 1879.

The story of creation, revisited

Just as our inductive definition defines the naturals in terms of the naturals, so does our recursive definition define addition in terms of addition.

Again, it is possible to assign our definition a meaning without resorting to unpermitted circularities. We do so by reducing our definition to equivalent inference rules for judgments about equality:

n : ℕ
--------------
zero + n  =  n

m + n  =  p
---------------------
(suc m) + n  =  suc p

Here we assume we have already defined the infinite set of natural numbers, specifying the meaning of the judgment n : ℕ. The first inference rule is the base case. It asserts that if n is a natural number then adding zero to it gives n. The second inference rule is the inductive case. It asserts that if adding m and n gives p, then adding suc m and n gives suc p.

Again we resort to a creation story, where this time we are concerned with judgments about addition:

-- In the beginning, we know nothing about addition.

Now, we apply the rules to all the judgment we know about. The base case tells us that zero + n = n for every natural n, so we add all those equations. The inductive case tells us that if m + n = p (on the day before today) then suc m + n = suc p (today). We didn’t know any equations about addition before today, so that rule doesn’t give us any new equations:

-- On the first day, we know about addition of 0.
0 + 0 = 0     0 + 1 = 1    0 + 2 = 2     ...

Then we repeat the process, so on the next day we know about all the equations from the day before, plus any equations added by the rules. The base case tells us nothing new, but now the inductive case adds more equations:

-- On the second day, we know about addition of 0 and 1.
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...

And we repeat the process again:

-- On the third day, we know about addition of 0, 1, and 2.
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...
2 + 0 = 2     2 + 1 = 3     2 + 2 = 4     2 + 3 = 5     ...

You’ve got the hang of it by now:

-- On the fourth day, we know about addition of 0, 1, 2, and 3.
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...
2 + 0 = 2     2 + 1 = 3     2 + 2 = 4     2 + 3 = 5     ...
3 + 0 = 3     3 + 1 = 4     3 + 2 = 5     3 + 3 = 6     ...

The process continues. On the m’th day we will know all the equations where the first number is less than m.

As we can see, the reasoning that justifies inductive and recursive definitions is quite similar. They might be considered two sides of the same coin.

The story of creation, finitely

The above story was told in a stratified way. First, we create the infinite set of naturals. We take that set as given when creating instances of addition, so even on day one we have an infinite set of instances.

Instead, we could choose to create both the naturals and the instances of addition at the same time. Then on any day there would be only a finite set of instances:

-- In the beginning, we know nothing.

Now, we apply the rules to all the judgment we know about. Only the base case for naturals applies:

-- On the first day, we know zero.
0 : ℕ

Again, we apply all the rules we know. This gives us a new natural, and our first equation about addition.

-- On the second day, we know one and all sums that yield zero.
0 : ℕ
1 : ℕ    0 + 0 = 0

Then we repeat the process. We get one more equation about addition from the base case, and also get an equation from the inductive case, applied to equation of the previous day:

-- On the third day, we know two and all sums that yield one.
0 : ℕ
1 : ℕ    0 + 0 = 0
2 : ℕ    0 + 1 = 1   1 + 0 = 1

You’ve got the hang of it by now:

-- On the fourth day, we know three and all sums that yield two.
0 : ℕ
1 : ℕ    0 + 0 = 0
2 : ℕ    0 + 1 = 1   1 + 0 = 1
3 : ℕ    0 + 2 = 2   1 + 1 = 2    2 + 0 = 2

On the n’th day there will be n distinct natural numbers, and n × (n-1) / 2 equations about addition. The number n and all equations for addition of numbers less than n first appear by day n+1. This gives an entirely finitist view of infinite sets of data and equations relating the data.

Writing definitions interactively

Agda is designed to be used with the Emacs text editor, and the two in combination provide features that help to create definitions and proofs interactively.

Begin by typing:

_+_ : ℕ → ℕ → ℕ
m + n = ?

The question mark indicates that you would like Agda to help with filling in that part of the code. If you type C-c C-l (pressing the control key while hitting the c key followed by the l key), which stands for load, the question mark will be replaced:

_+_ : ℕ → ℕ → ℕ
m + n = { }0

The empty braces are called a hole, and 0 is a number used for referring to the hole. The hole will display highlighted in green. Emacs will also create a window displaying the text

?0 : ℕ

to indicate that hole 0 is to be filled in with a term of type ℕ. Typing C-c C-f (for forward) will move you into the next hole.

We wish to define addition by recursion on the first argument. Move the cursor into the hole and type C-c C-c (for case). You will be given the prompt:

pattern variables to case (empty for split on result):

Typing m will cause a split on that variable, resulting in an update to the code:

_+_ : ℕ → ℕ → ℕ
zero + n = { }0
suc m + n = { }1

There are now two holes, and the window at the bottom tells you the required type of each:

?0 : ℕ
?1 : ℕ

Going into hole 0 and typing C-c C-, will display information on the required type of the hole, and what free variables are available:

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ

This strongly suggests filling the hole with n. After the hole is filled, you can type C-c C-space, which will remove the hole:

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = { }1

Again, going into hole 1 and typing C-c C-, will display information on the required type of the hole, and what free variables are available:

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ

Going into the hole and type C-c C-r (for refine) will fill it in with a constructor (if there is a unique choice) or tell you what constructors you might use, if there is a choice. In this case, it displays the following:

Don't know which constructor to introduce of zero or suc

Filling the hole with suc ? and typing C-c C-space results in the following:

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc { }1

Going into the new hole and typing C-c C-, gives similar information to before:

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ

We can fill the hole with m + n and type C-c C-space to complete the program:

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

Exploiting interaction to this degree is probably not helpful for a program this simple, but the same techniques can help with more complex programs. Even for a program this simple, using C-c C-c to split cases can be helpful.

More pragmas

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

tells Agda that these three operators correspond to the usual ones, and enables it to perform these computations using the corresponding Haskell operators on the arbitrary-precision integer type. Representing naturals with zero and suc requires time proportional to m to add m and n, whereas representing naturals as integers in Haskell requires time proportional to the larger of the logarithms of m and n. Similarly, representing naturals with zero and suc requires time proportional to the product of m and n to multiply m and n, whereas representing naturals as integers in Haskell requires time proportional to the sum of the logarithms of m and n.

Exercise Bin (stretch)

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

For instance, the bitstring

1011

standing for the number eleven is encoded as

⟨⟩ I O I I

Representations are not unique due to leading zeros. Hence, eleven is also represented by 001011, encoded as:

⟨⟩ O O I O I I

Define a function

inc : Bin → Bin

that converts a bitstring to the bitstring for the next higher number. For example, since 1100 encodes twelve, we should have:

inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O

Confirm that this gives the correct answer for the bitstrings encoding zero through four.

Using the above, define a pair of functions to convert between the two representations.

to   : ℕ → Bin
from : Bin → ℕ

For the former, choose the bitstring to have no leading zeros if it represents a positive natural, and represent zero by ⟨⟩ O. Confirm that these both give the correct answer for zero through four.

-- Your code goes here

Standard library

At the end of each chapter, we will show where to find relevant definitions in the standard library. The naturals, constructors for them, and basic operators upon them, are defined in the standard library module Data.Nat:

-- import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)

Normally, we will show an import as running code, so Agda will complain if we attempt to import a definition that is not available. This time, however, we have only shown the import as a comment. Both this chapter and the standard library invoke the NATURAL pragma, the former on ℕ, and the latter on the equivalent type Data.Nat.ℕ. Such a pragma can only be invoked once, as invoking it twice would raise confusion as to whether 2 is a value of type ℕ or type Data.Nat.ℕ. Similar confusions arise if other pragmas are invoked twice. For this reason, we will usually avoid pragmas in future chapters. Information on pragmas can be found in the Agda documentation.

Unicode

This chapter uses the following unicode:

ℕ  U+2115  DOUBLE-STRUCK CAPITAL N (\bN)
→  U+2192  RIGHTWARDS ARROW (\to, \r, \->)
∸  U+2238  DOT MINUS (\.-)
≡  U+2261  IDENTICAL TO (\==)
⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
∎  U+220E  END OF PROOF (\qed)

Each line consists of the Unicode character (ℕ), the corresponding code point (U+2115), the name of the character (DOUBLE-STRUCK CAPITAL N), and the sequence to type into Emacs to generate the character (\bN).

The command \r gives access to a wide variety of rightward arrows. After typing \r, one can access the many available arrows by using the left, right, up, and down keys to navigate. The command remembers where you navigated to the last time, and starts with the same character next time. The command \l works similarly for left arrows. In place of left, right, up, and down keys, one may also use control characters:

C-b  left (backward one character)
C-f  right (forward one character)
C-p  up (to the previous line)
C-n  down (to the next line)

We write C-b to stand for control-b, and similarly. One can also navigate left and right by typing the digits that appear in the displayed list.

For a full list of supported characters, use agda-input-show-translations with:

M-x agda-input-show-translations

All the characters supported by agda-mode are shown. We write M-x to stand for typing ESC followed by x.

If you want to know how you input a specific Unicode character in an agda file, move the cursor onto the character and use quail-show-key with:

M-x quail-show-key

You’ll see a key sequence of the character in mini buffer. If you run M-x quail-show-key on say ∸, you will see \.- for the character.

Induction: Proof by Induction

module plfa.part1.Induction where

Induction makes you feel guilty for getting something out of nothing … but it is one of the greatest ideas of civilization. – Herbert Wilf

Now that we’ve defined the naturals and operations upon them, our next step is to learn how to prove properties that they satisfy. As hinted by their name, properties of inductive datatypes are proved by induction.

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

(Importing step-≡ defines _≡⟨_⟩_.)

Properties of operators

Operators pop up all the time, and mathematicians have agreed on names for some of the most common properties.

• Identity. Operator + has left identity 0 if 0 + n ≡ n, and right identity 0 if n + 0 ≡ n, for all n. A value that is both a left and right identity is just called an identity. Identity is also sometimes called unit.

• Associativity. Operator + is associative if the location of parentheses does not matter: (m + n) + p ≡ m + (n + p), for all m, n, and p.

• Commutativity. Operator + is commutative if order of arguments does not matter: m + n ≡ n + m, for all m and n.

• Distributivity. Operator * distributes over operator + from the left if m * (p + q) ≡ (m * p) + (m * q), for all m, p, and q, and from the right if (m + n) * p ≡ (m * p) + (n * p), for all m, n, and p.

Addition has identity 0 and multiplication has identity 1; addition and multiplication are both associative and commutative; and multiplication distributes over addition.

If you ever bump into an operator at a party, you now know how to make small talk, by asking whether it has a unit and is associative or commutative. If you bump into two operators, you might ask them if one distributes over the other.

Less frivolously, if you ever bump into an operator while reading a technical paper, this gives you a way to orient yourself, by checking whether or not it has an identity, is associative or commutative, or distributes over another operator. A careful author will often call out these properties—or their lack—for instance by pointing out that a newly introduced operator is associative but not commutative.

Exercise operators (practice)

Give another example of a pair of operators that have an identity and are associative, commutative, and distribute over one another. (You do not have to prove these properties.)

Give an example of an operator that has an identity and is associative but is not commutative. (You do not have to prove these properties.)

Associativity

One property of addition is that it is associative, that is, that the location of the parentheses does not matter:

(m + n) + p ≡ m + (n + p)

Here m, n, and p are variables that range over all natural numbers.

_ : ( + ) +  ≡  + ( + )
_ =
  begin
    ( + ) + 
  ≡⟨⟩
     + 
  ≡⟨⟩
    
  ≡⟨⟩
     + 
  ≡⟨⟩
     + ( + )
  ∎

Here we have displayed the computation as a chain of equations, one term to a line. It is often easiest to read such chains from the top down until one reaches the simplest term (in this case, 12), and then from the bottom up until one reaches the same term.

The test reveals that associativity is perhaps not as obvious as first it appears. Why should 7 + 5 be the same as 3 + 9? We might want to gather more evidence, testing the proposition by choosing other numbers. But—since there are an infinite number of naturals—testing can never be complete. Is there any way we can be sure that associativity holds for all the natural numbers?

The answer is yes! We can prove a property holds for all naturals using proof by induction.

Proof by induction

Recall the definition of natural numbers consists of a base case which tells us that zero is a natural, and an inductive case which tells us that if m is a natural then suc m is also a natural.

Proof by induction follows the structure of this definition. To prove a property of natural numbers by induction, we need to prove two cases. First is the base case, where we show the property holds for zero. Second is the inductive case, where we assume the property holds for an arbitrary natural m (we call this the inductive hypothesis), and then show that the property must also hold for suc m.

If we write P m for a property of m, then what we need to demonstrate are the following two inference rules:

------
P zero

P m
---------
P (suc m)

Let’s unpack these rules. The first rule is the base case, and requires we show that property P holds for zero. The second rule is the inductive case, and requires we show that if we assume the inductive hypothesis—namely that P holds for m—then it follows that P also holds for suc m.

Why does this work? Again, it can be explained by a creation story. To start with, we know no properties:

-- In the beginning, no properties are known.

Now, we apply the two rules to all the properties we know about. The base case tells us that P zero holds, so we add it to the set of known properties. The inductive case tells us that if P m holds (on the day before today) then P (suc m) also holds (today). We didn’t know about any properties before today, so the inductive case doesn’t apply:

-- On the first day, one property is known.
P zero

Then we repeat the process, so on the next day we know about all the properties from the day before, plus any properties added by the rules. The base case tells us that P zero holds, but we already knew that. But now the inductive case tells us that since P zero held yesterday, then P (suc zero) holds today:

-- On the second day, two properties are known.
P zero
P (suc zero)

And we repeat the process again. Now the inductive case tells us that since P zero and P (suc zero) both hold, then P (suc zero) and P (suc (suc zero)) also hold. We already knew about the first of these, but the second is new:

-- On the third day, three properties are known.
P zero
P (suc zero)
P (suc (suc zero))

You’ve got the hang of it by now:

-- On the fourth day, four properties are known.
P zero
P (suc zero)
P (suc (suc zero))
P (suc (suc (suc zero)))

The process continues. On the n’th day there will be n distinct properties that hold. The property of every natural number will appear on some given day. In particular, the property P n first appears on day n+1.

Our first proof: associativity

To prove associativity, we take P m to be the property:

(m + n) + p ≡ m + (n + p)

Here n and p are arbitrary natural numbers, so if we can show the equation holds for all m it will also hold for all n and p. The appropriate instances of the inference rules are:

-------------------------------
(zero + n) + p ≡ zero + (n + p)

(m + n) + p ≡ m + (n + p)
---------------------------------
(suc m + n) + p ≡ suc m + (n + p)

If we can demonstrate both of these, then associativity of addition follows by induction.

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

We have named the proof +-assoc. In Agda, identifiers can consist of any sequence of characters not including spaces or the characters @.(){};_.

Let’s unpack this code. The signature states that we are defining the identifier +-assoc which provides evidence for the proposition:

∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

The upside down A is pronounced “for all”, and the proposition asserts that for all natural numbers m, n, and p the equation (m + n) + p ≡ m + (n + p) holds. Evidence for the proposition is a function that accepts three natural numbers, binds them to m, n, and p, and returns evidence for the corresponding instance of the equation.

For the base case, we must show:

(zero + n) + p ≡ zero + (n + p)

Simplifying both sides with the base case of addition yields the equation:

n + p ≡ n + p

This holds trivially. Reading the chain of equations in the base case of the proof, the top and bottom of the chain match the two sides of the equation to be shown, and reading down from the top and up from the bottom takes us to n + p in the middle. No justification other than simplification is required.

For the inductive case, we must show:

(suc m + n) + p ≡ suc m + (n + p)

Simplifying both sides with the inductive case of addition yields the equation:

suc ((m + n) + p) ≡ suc (m + (n + p))

This in turn follows by prefacing suc to both sides of the induction hypothesis:

(m + n) + p ≡ m + (n + p)

Reading the chain of equations in the inductive case of the proof, the top and bottom of the chain match the two sides of the equation to be shown, and reading down from the top and up from the bottom takes us to the simplified equation above. The remaining equation does not follow from simplification alone, so we use an additional operator for chain reasoning, _≡⟨_⟩_, where a justification for the equation appears within angle brackets. The justification given is:

⟨ cong suc (+-assoc m n p) ⟩

Here, the recursive invocation +-assoc m n p has as its type the induction hypothesis, and cong suc prefaces suc to each side to yield the needed equation.

A relation is said to be a congruence for a given function if it is preserved by applying that function. If e is evidence that x ≡ y, then cong f e is evidence that f x ≡ f y, for any function f.

Here the inductive hypothesis is not assumed, but instead proved by a recursive invocation of the function we are defining, +-assoc m n p. As with addition, this is well founded because associativity of larger numbers is proved in terms of associativity of smaller numbers. In this case, assoc (suc m) n p is proved using assoc m n p. The correspondence between proof by induction and definition by recursion is one of the most appealing aspects of Agda.

Induction as recursion

As a concrete example of how induction corresponds to recursion, here is the computation that occurs when instantiating m to 2 in the proof of associativity.

+-assoc-2 : ∀ (n p : ℕ) → ( + n) + p ≡  + (n + p)
+-assoc-2 n p =
  begin
    ( + n) + p
  ≡⟨⟩
    suc ( + n) + p
  ≡⟨⟩
    suc (( + n) + p)
  ≡⟨ cong suc (+-assoc-1 n p) ⟩
    suc ( + (n + p))
  ≡⟨⟩
     + (n + p)
  ∎
  where
  +-assoc-1 : ∀ (n p : ℕ) → ( + n) + p ≡  + (n + p)
  +-assoc-1 n p =
    begin
      ( + n) + p
    ≡⟨⟩
      suc ( + n) + p
    ≡⟨⟩
      suc (( + n) + p)
    ≡⟨ cong suc (+-assoc-0 n p) ⟩
      suc ( + (n + p))
    ≡⟨⟩
       + (n + p)
    ∎
    where
    +-assoc-0 : ∀ (n p : ℕ) → ( + n) + p ≡  + (n + p)
    +-assoc-0 n p =
      begin
        ( + n) + p
      ≡⟨⟩
        n + p
      ≡⟨⟩
         + (n + p)
      ∎

Terminology and notation

The symbol ∀ appears in the statement of associativity to indicate that it holds for all numbers m, n, and p. We refer to ∀ as the universal quantifier, and it is discussed further in Chapter Quantifiers.

Evidence for a universal quantifier is a function. The notations

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

and

+-assoc : ∀ (m : ℕ) → ∀ (n : ℕ) → ∀ (p : ℕ) → (m + n) + p ≡ m + (n + p)

are equivalent. They differ from a function type such as ℕ → ℕ → ℕ in that variables are associated with each argument type, and the result type may mention (or depend upon) these variables; hence they are called dependent functions.

Our second proof: commutativity

Another important property of addition is that it is commutative, that is, that the order of the operands does not matter:

m + n ≡ n + m

The proof requires that we first demonstrate two lemmas.

The first lemma

The base case of the definition of addition states that zero is a left-identity:

zero + n ≡ n

Our first lemma states that zero is also a right-identity:

m + zero ≡ m

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
  ∎

The signature states that we are defining the identifier +-identityʳ which provides evidence for the proposition:

∀ (m : ℕ) → m + zero ≡ m

Evidence for the proposition is a function that accepts a natural number, binds it to m, and returns evidence for the corresponding instance of the equation. The proof is by induction on m.

For the base case, we must show:

zero + zero ≡ zero

Simplifying with the base case of addition, this is straightforward.

For the inductive case, we must show:

(suc m) + zero = suc m

Simplifying both sides with the inductive case of addition yields the equation:

suc (m + zero) = suc m

This in turn follows by prefacing suc to both sides of the induction hypothesis:

m + zero ≡ m

Reading the chain of equations down from the top and up from the bottom takes us to the simplified equation above. The remaining equation has the justification:

⟨ cong suc (+-identityʳ m) ⟩

Here, the recursive invocation +-identityʳ m has as its type the induction hypothesis, and cong suc prefaces suc to each side to yield the needed equation. This completes the first lemma.

The second lemma

The inductive case of the definition of addition pushes suc on the first argument to the outside:

suc m + n ≡ suc (m + n)

Our second lemma does the same for suc on the second argument:

m + suc n ≡ suc (m + n)

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

The signature states that we are defining the identifier +-suc which provides evidence for the proposition:

∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

Evidence for the proposition is a function that accepts two natural numbers, binds them to m and n, and returns evidence for the corresponding instance of the equation. The proof is by induction on m.

For the base case, we must show:

zero + suc n ≡ suc (zero + n)

Simplifying with the base case of addition, this is straightforward.

For the inductive case, we must show:

suc m + suc n ≡ suc (suc m + n)

Simplifying both sides with the inductive case of addition yields the equation:

suc (m + suc n) ≡ suc (suc (m + n))

This in turn follows by prefacing suc to both sides of the induction hypothesis:

m + suc n ≡ suc (m + n)

Reading the chain of equations down from the top and up from the bottom takes us to the simplified equation in the middle. The remaining equation has the justification:

⟨ cong suc (+-suc m n) ⟩

Here, the recursive invocation +-suc m n has as its type the induction hypothesis, and cong suc prefaces suc to each side to yield the needed equation. This completes the second lemma.

The proposition

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

The first line states that we are defining the identifier +-comm which provides evidence for the proposition:

∀ (m n : ℕ) → m + n ≡ n + m

Evidence for the proposition is a function that accepts two natural numbers, binds them to m and n, and returns evidence for the corresponding instance of the equation. The proof is by induction on n. (Not on m this time!)

For the base case, we must show:

m + zero ≡ zero + m

Simplifying both sides with the base case of addition yields the equation:

m + zero ≡ m

The remaining equation has the justification ⟨ +-identityʳ m ⟩, which invokes the first lemma.

For the inductive case, we must show:

m + suc n ≡ suc n + m

Simplifying both sides with the inductive case of addition yields the equation:

m + suc n ≡ suc (n + m)

We show this in two steps. First, we have:

m + suc n ≡ suc (m + n)

which is justified by the second lemma, ⟨ +-suc m n ⟩. Then we have

suc (m + n) ≡ suc (n + m)

which is justified by congruence and the induction hypothesis, ⟨ cong suc (+-comm m n) ⟩. This completes the proof.

Agda requires that identifiers are defined before they are used, so we must present the lemmas before the main proposition, as we have done above. In practice, one will often attempt to prove the main proposition first, and the equations required to do so will suggest what lemmas to prove.

Our first corollary: rearranging

+-rearrange : ∀ (m n p q : ℕ) → (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange m n p q =
  begin
    (m + n) + (p + q)
  ≡⟨ sym (+-assoc (m + n) p q) ⟩
    ((m + n) + p) + q
  ≡⟨ cong (_+ q) (+-assoc m n p) ⟩
    (m + (n + p)) + q
  ∎

No induction is required, we simply apply associativity twice. A few points are worthy of note.

First, addition associates to the left, so m + (n + p) + q stands for (m + (n + p)) + q.

Second, we use sym to interchange the sides of an equation. Proposition +-assoc (m + n) p q shifts parentheses from left to right:

((m + n) + p) + q ≡ (m + n) + (p + q)

To shift them the other way, we use sym (+-assoc n p q):

(m + n) + (p + q) ≡ ((m + n) + p) + q

In general, if e provides evidence for x ≡ y then sym e provides evidence for y ≡ x.

Third, Agda supports a variant of the section notation introduced by Richard Bird. We write (_+ y) for the function that applied to x returns x + y. Thus, applying the congruence cong (_+ q) to assoc m n p takes the equation:

(m + n) + p  ≡  m + (n + p)

into the equation:

((m + n) + p) + q  ≡  (m + (n + p)) + q

Similarly, we write (x +_) for the function that applied to y returns x + y; the same works for any infix operator.

Creation, one last time

Returning to the proof of associativity, it may be helpful to view the inductive proof (or, equivalently, the recursive definition) as a creation story. This time we are concerned with judgments asserting associativity:

 -- In the beginning, we know nothing about associativity.

Now, we apply the rules to all the judgments we know about. The base case tells us that (zero + n) + p ≡ zero + (n + p) for every natural n and p. The inductive case tells us that if (m + n) + p ≡ m + (n + p) (on the day before today) then (suc m + n) + p ≡ suc m + (n + p) (today). We didn’t know any judgments about associativity before today, so that rule doesn’t give us any new judgments:

-- On the first day, we know about associativity of 0.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...

Then we repeat the process, so on the next day we know about all the judgments from the day before, plus any judgments added by the rules. The base case tells us nothing new, but now the inductive case adds more judgments:

-- On the second day, we know about associativity of 0 and 1.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...

And we repeat the process again:

-- On the third day, we know about associativity of 0, 1, and 2.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...
(2 + 0) + 0 ≡ 2 + (0 + 0)   ...   (2 + 4) + 5 ≡ 2 + (4 + 5)   ...

You’ve got the hang of it by now:

-- On the fourth day, we know about associativity of 0, 1, 2, and 3.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...
(2 + 0) + 0 ≡ 2 + (0 + 0)   ...   (2 + 4) + 5 ≡ 2 + (4 + 5)   ...
(3 + 0) + 0 ≡ 3 + (0 + 0)   ...   (3 + 4) + 5 ≡ 3 + (4 + 5)   ...

The process continues. On the m’th day we will know all the judgments where the first number is less than m.

There is also a completely finite approach to generating the same equations, which is left as an exercise for the reader.

Exercise finite-+-assoc (stretch)

Write out what is known about associativity of addition on each of the first four days using a finite story of creation, as earlier.

-- Your code goes here

Associativity with rewrite

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero    n p                          =  refl
+-assoc′ (suc m) n p  rewrite +-assoc′ m n p  =  refl

For the base case, we must show:

(zero + n) + p ≡ zero + (n + p)

Simplifying both sides with the base case of addition yields the equation:

n + p ≡ n + p

This holds trivially. The proof that a term is equal to itself is written refl.

For the inductive case, we must show:

(suc m + n) + p ≡ suc m + (n + p)

Simplifying both sides with the inductive case of addition yields the equation:

suc ((m + n) + p) ≡ suc (m + (n + p))

This is our goal to be proved. Rewriting by a given equation is indicated by the keyword rewrite followed by a proof of that equation. Rewriting replaces each occurrence of the left-hand side of the equation in the goal by the right-hand side. In this case, after rewriting by the inductive hypothesis our goal becomes

suc (m + (n + p)) ≡ suc (m + (n + p))

and the proof is again given by refl. Rewriting avoids not only chains of equations but also the need to invoke cong.

Commutativity with rewrite

+-identity′ : ∀ (n : ℕ) → n + zero ≡ n
+-identity′ zero = refl
+-identity′ (suc n) rewrite +-identity′ n = refl

+-suc′ : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc′ zero n = refl
+-suc′ (suc m) n rewrite +-suc′ m n = refl

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ m zero rewrite +-identity′ m = refl
+-comm′ m (suc n) rewrite +-suc′ m n | +-comm′ m n = refl

In the final line, rewriting with two equations is indicated by separating the two proofs of the relevant equations by a vertical bar; the rewrite on the left is performed before that on the right.

Building proofs interactively

It is instructive to see how to build the alternative proof of associativity using the interactive features of Agda in Emacs. Begin by typing:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ m n p = ?

The question mark indicates that you would like Agda to help with filling in that part of the code. If you type C-c C-l (control-c followed by control-l), the question mark will be replaced:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ m n p = { }0

The empty braces are called a hole, and 0 is a number used for referring to the hole. The hole may display highlighted in green. Emacs will also create a new window at the bottom of the screen displaying the text:

?0 : ((m + n) + p) ≡ (m + (n + p))

This indicates that hole 0 is to be filled in with a proof of the stated judgment.

We wish to prove the proposition by induction on m. Move the cursor into the hole and type C-c C-c. You will be given the prompt:

pattern variables to case (empty for split on result):

Typing m will cause a split on that variable, resulting in an update to the code:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = { }0
+-assoc′ (suc m) n p = { }1

There are now two holes, and the window at the bottom tells you what each is required to prove:

?0 : ((zero + n) + p) ≡ (zero + (n + p))
?1 : ((suc m + n) + p) ≡ (suc m + (n + p))

Going into hole 0 and typing C-c C-, will display the text:

Goal: (n + p) ≡ (n + p)
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ

This indicates that after simplification the goal for hole 0 is as stated, and that variables p and n of the stated types are available to use in the proof. The proof of the given goal is trivial, and going into the goal and typing C-c C-r will fill it in. Typing C-c C-l renumbers the remaining hole to 0:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p = { }0

Going into the new hole 0 and typing C-c C-, will display the text:

Goal: suc ((m + n) + p) ≡ suc (m + (n + p))
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ
m : ℕ

Again, this gives the simplified goal and the available variables. In this case, we need to rewrite by the induction hypothesis, so let’s edit the text accordingly:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = { }0

Going into the remaining hole and typing C-c C-, will display the text:

Goal: suc (m + (n + p)) ≡ suc (m + (n + p))
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ
m : ℕ

The proof of the given goal is trivial, and going into the goal and typing C-c C-r will fill it in, completing the proof:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl

Exercise +-swap (recommended)

Show

m + (n + p) ≡ n + (m + p)

for all naturals m, n, and p. No induction is needed, just apply the previous results which show addition is associative and commutative.

-- Your code goes here

Exercise *-distrib-+ (recommended)

Show multiplication distributes over addition, that is,

(m + n) * p ≡ m * p + n * p

for all naturals m, n, and p.

-- Your code goes here

Exercise *-assoc (recommended)

Show multiplication is associative, that is,

(m * n) * p ≡ m * (n * p)

for all naturals m, n, and p.

-- Your code goes here

Exercise *-comm (practice)

Show multiplication is commutative, that is,

m * n ≡ n * m

for all naturals m and n. As with commutativity of addition, you will need to formulate and prove suitable lemmas.

-- Your code goes here

Exercise 0∸n≡0 (practice)

Show

zero ∸ n ≡ zero

for all naturals n. Did your proof require induction?

-- Your code goes here

Exercise ∸-+-assoc (practice)

Show that monus associates with addition, that is,

m ∸ n ∸ p ≡ m ∸ (n + p)

for all naturals m, n, and p.

-- Your code goes here

Exercise +*^ (stretch)

Show the following three laws

 m ^ (n + p) ≡ (m ^ n) * (m ^ p)  (^-distribˡ-+-*)
 (m * n) ^ p ≡ (m ^ p) * (n ^ p)  (^-distribʳ-*)
 (m ^ n) ^ p ≡ m ^ (n * p)        (^-*-assoc)

for all m, n, and p.

-- Your code goes here

Exercise Bin-laws (stretch)

Recall that Exercise Bin defines a datatype Bin of bitstrings representing natural numbers, and asks you to define functions

inc   : Bin → Bin
to    : ℕ → Bin
from  : Bin → ℕ

Consider the following laws, where n ranges over naturals and b over bitstrings:

from (inc b) ≡ suc (from b)
to (from b) ≡ b
from (to n) ≡ n

For each law: if it holds, prove; if not, give a counterexample.

-- Your code goes here

Standard library

import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)

Unicode

This chapter uses the following unicode:

∀  U+2200  FOR ALL (\forall, \all)
ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)
′  U+2032  PRIME (\')
″  U+2033  DOUBLE PRIME (\')
‴  U+2034  TRIPLE PRIME (\')
⁗  U+2057  QUADRUPLE PRIME (\')

Similar to \r, the command \^r gives access to a variety of superscript rightward arrows, and also a superscript letter r. The command \' gives access to a range of primes (′ ″ ‴ ⁗).

Relations: Inductive definition of relations

module plfa.part1.Relations where

After having defined operations such as addition and multiplication, the next step is to define relations, such as less than or equal.

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm; +-identityʳ)

Defining relations

The relation less than or equal has an infinite number of instances. Here are a few of them:

0 ≤ 0     0 ≤ 1     0 ≤ 2     0 ≤ 3     ...
          1 ≤ 1     1 ≤ 2     1 ≤ 3     ...
                    2 ≤ 2     2 ≤ 3     ...
                              3 ≤ 3     ...
                                        ...

And yet, we can write a finite definition that encompasses all of these instances in just a few lines. Here is the definition as a pair of inference rules:

z≤n --------
    zero ≤ n

    m ≤ n
s≤s -------------
    suc m ≤ suc n

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

Here z≤n and s≤s (with no spaces) are constructor names, while zero ≤ n, and m ≤ n and suc m ≤ suc n (with spaces) are types. This is our first use of an indexed datatype, where the type m ≤ n is indexed by two naturals, m and n. In Agda any line beginning with two or more dashes is a comment, and here we have exploited that convention to write our Agda code in a form that resembles the corresponding inference rules, a trick we will use often from now on.

Both definitions above tell us the same two things:

• Base case: for all naturals n, the proposition zero ≤ n holds.
• Inductive case: for all naturals m and n, if the proposition m ≤ n holds, then the proposition suc m ≤ suc n holds.

In fact, they each give us a bit more detail:

• Base case: for all naturals n, the constructor z≤n produces evidence that zero ≤ n holds.
• Inductive case: for all naturals m and n, the constructor s≤s takes evidence that m ≤ n holds into evidence that suc m ≤ suc n holds.

For example, here in inference rule notation is the proof that 2 ≤ 4:

  z≤n -----
      0 ≤ 2
 s≤s -------
      1 ≤ 3
s≤s ---------
      2 ≤ 4

_ :  ≤ 
_ = s≤s (s≤s z≤n)

Implicit arguments

This is our first use of implicit arguments. In the definition of inequality, the two lines defining the constructors use ∀, very similar to our use of ∀ in propositions such as:

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m

However, here the declarations are surrounded by curly braces { } rather than parentheses ( ). This means that the arguments are implicit and need not be written explicitly; instead, they are inferred by Agda’s typechecker. Thus, we write +-comm m n for the proof that m + n ≡ n + m, but z≤n for the proof that zero ≤ n, leaving n implicit. Similarly, if m≤n is evidence that m ≤ n, we write s≤s m≤n for evidence that suc m ≤ suc n, leaving both m and n implicit.

_ :  ≤ 
_ = s≤s {} {} (s≤s {} {} (z≤n {}))

_ :  ≤ 
_ = s≤s {m = } {n = } (s≤s {m = } {n = } (z≤n {n = }))

_ :  ≤ 
_ = s≤s {n = } (s≤s {n = } z≤n)

It is not permitted to swap implicit arguments, even when named.

+-identityʳ′ : ∀ {m : ℕ} → m + zero ≡ m
+-identityʳ′ = +-identityʳ _

We use _ to ask Agda to infer the value of the explicit argument from context. There is only one value which gives us the correct proof, m, so Agda happily fills it in. If Agda fails to infer the value, it reports an error.

Precedence

infix  _≤_

We set the precedence of _≤_ at level 4, so it binds less tightly than _+_ at level 6 and hence 1 + 2 ≤ 3 parses as (1 + 2) ≤ 3. We write infix to indicate that the operator does not associate to either the left or right, as it makes no sense to parse 1 ≤ 2 ≤ 3 as either (1 ≤ 2) ≤ 3 or 1 ≤ (2 ≤ 3).

Decidability

Given two numbers, it is straightforward to compute whether or not the first is less than or equal to the second. We don’t give the code for doing so here, but will return to this point in Chapter Decidable.

Inversion

In our definitions, we go from smaller things to larger things. For instance, from m ≤ n we can conclude suc m ≤ suc n, where suc m is bigger than m (that is, the former contains the latter), and suc n is bigger than n. But sometimes we want to go from bigger things to smaller things.

inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
    -------------
  → m ≤ n
inv-s≤s (s≤s m≤n) = m≤n

Here m≤n (with no spaces) is a variable name while m ≤ n (with spaces) is a type, and the latter is the type of the former. It is a common convention in Agda to derive a variable name by removing spaces from its type.

Not every rule is invertible; indeed, the rule for z≤n has no non-implicit hypotheses, so there is nothing to invert. But often inversions of this kind hold.

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
    --------
  → m ≡ zero
inv-z≤n z≤n = refl

Properties of ordering relations

Relations pop up all the time, and mathematicians have agreed on names for some of the most common properties.

• Reflexive. For all n, the relation n ≤ n holds.
• Transitive. For all m, n, and p, if m ≤ n and n ≤ p hold, then m ≤ p holds.
• Anti-symmetric. For all m and n, if both m ≤ n and n ≤ m hold, then m ≡ n holds.
• Total. For all m and n, either m ≤ n or n ≤ m holds.

The relation _≤_ satisfies all four of these properties.

There are also names for some combinations of these properties.

• Preorder. Any relation that is reflexive and transitive.
• Partial order. Any preorder that is also anti-symmetric.
• Total order. Any partial order that is also total.

If you ever bump into a relation at a party, you now know how to make small talk, by asking it whether it is reflexive, transitive, anti-symmetric, and total. Or instead you might ask whether it is a preorder, partial order, or total order.

Less frivolously, if you ever bump into a relation while reading a technical paper, this gives you a way to orient yourself, by checking whether or not it is a preorder, partial order, or total order. A careful author will often call out these properties—or their lack—for instance by saying that a newly introduced relation is a partial order but not a total order.

Exercise orderings (practice)

Give an example of a preorder that is not a partial order.

-- Your code goes here

Give an example of a partial order that is not a total order.

-- Your code goes here

Reflexivity

≤-refl : ∀ {n : ℕ}
    -----
  → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

The proof is a straightforward induction on the implicit argument n. In the base case, zero ≤ zero holds by z≤n. In the inductive case, the inductive hypothesis ≤-refl {n} gives us a proof of n ≤ n, and applying s≤s to that yields a proof of suc n ≤ suc n.

It is a good exercise to prove reflexivity interactively in Emacs, using holes and the C-c C-c, C-c C-,, and C-c C-r commands.

Transitivity

≤-trans : ∀ {m n p : ℕ}
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans z≤n       _          =  z≤n
≤-trans (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans m≤n n≤p)

Here the proof is by induction on the evidence that m ≤ n. In the base case, the first inequality holds by z≤n and must show zero ≤ p, which follows immediately by z≤n. In this case, the fact that n ≤ p is irrelevant, and we write _ as the pattern to indicate that the corresponding evidence is unused.

In the inductive case, the first inequality holds by s≤s m≤n and the second inequality by s≤s n≤p, and so we are given suc m ≤ suc n and suc n ≤ suc p, and must show suc m ≤ suc p. The inductive hypothesis ≤-trans m≤n n≤p establishes that m ≤ p, and our goal follows by applying s≤s.

The case ≤-trans (s≤s m≤n) z≤n cannot arise, since the first inequality implies the middle value is suc n while the second inequality implies that it is zero. Agda can determine that such a case cannot arise, and does not require (or permit) it to be listed.

≤-trans′ : ∀ (m n p : ℕ)
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans′ zero    _       _       z≤n       _          =  z≤n
≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans′ m n p m≤n n≤p)

One might argue that this is clearer or one might argue that the extra length obscures the essence of the proof. We will usually opt for shorter proofs.

The technique of induction on evidence that a property holds (e.g., inducting on evidence that m ≤ n)—rather than induction on values of which the property holds (e.g., inducting on m)—will turn out to be immensely valuable, and one that we use often.

Again, it is a good exercise to prove transitivity interactively in Emacs, using holes and the C-c C-c, C-c C-,, and C-c C-r commands.

Anti-symmetry

≤-antisym : ∀ {m n : ℕ}
  → m ≤ n
  → n ≤ m
    -----
  → m ≡ n
≤-antisym z≤n       z≤n        =  refl
≤-antisym (s≤s m≤n) (s≤s n≤m)  =  cong suc (≤-antisym m≤n n≤m)

Again, the proof is by induction over the evidence that m ≤ n and n ≤ m hold.

In the base case, both inequalities hold by z≤n, and so we are given zero ≤ zero and zero ≤ zero and must show zero ≡ zero, which follows by reflexivity. (Reflexivity of equality, that is, not reflexivity of inequality.)

In the inductive case, the first inequality holds by s≤s m≤n and the second inequality holds by s≤s n≤m, and so we are given suc m ≤ suc n and suc n ≤ suc m and must show suc m ≡ suc n. The inductive hypothesis ≤-antisym m≤n n≤m establishes that m ≡ n, and our goal follows by congruence.

Exercise ≤-antisym-cases (practice)

The above proof omits cases where one argument is z≤n and one argument is s≤s. Why is it ok to omit them?

-- Your code goes here

Total

The fourth property to prove about comparison is that it is total: for any naturals m and n either m ≤ n or n ≤ m, or both if m and n are equal.

data Total (m n : ℕ) : Set where

  forward :
      m ≤ n
      ---------
    → Total m n

  flipped :
      n ≤ m
      ---------
    → Total m n

Evidence that Total m n holds is either of the form forward m≤n or flipped n≤m, where m≤n and n≤m are evidence of m ≤ n and n ≤ m respectively.

(For those familiar with logic, the above definition could also be written as a disjunction. Disjunctions will be introduced in Chapter Connectives.)

data Total′ : ℕ → ℕ → Set where

  forward′ : ∀ {m n : ℕ}
    → m ≤ n
      ----------
    → Total′ m n

  flipped′ : ∀ {m n : ℕ}
    → n ≤ m
      ----------
    → Total′ m n

Each parameter of the type translates as an implicit parameter of each constructor. Unlike an indexed datatype, where the indexes can vary (as in zero ≤ n and suc m ≤ suc n), in a parameterised datatype the parameters must always be the same (as in Total m n). Parameterised declarations are shorter, easier to read, and occasionally aid Agda’s termination checker, so we will use them in preference to indexed types when possible.

≤-total : ∀ (m n : ℕ) → Total m n
≤-total zero    n                         =  forward z≤n
≤-total (suc m) zero                      =  flipped z≤n
≤-total (suc m) (suc n) with ≤-total m n
...                        | forward m≤n  =  forward (s≤s m≤n)
...                        | flipped n≤m  =  flipped (s≤s n≤m)

In this case the proof is by induction over both the first and second arguments. We perform a case analysis:

• First base case: If the first argument is zero and the second argument is n then the forward case holds, with z≤n as evidence that zero ≤ n.

• Second base case: If the first argument is suc m and the second argument is zero then the flipped case holds, with z≤n as evidence that zero ≤ suc m.

• Inductive case: If the first argument is suc m and the second argument is suc n, then the inductive hypothesis ≤-total m n establishes one of the following:

  • The forward case of the inductive hypothesis holds with m≤n as evidence that m ≤ n, from which it follows that the forward case of the proposition holds with s≤s m≤n as evidence that suc m ≤ suc n.

  • The flipped case of the inductive hypothesis holds with n≤m as evidence that n ≤ m, from which it follows that the flipped case of the proposition holds with s≤s n≤m as evidence that suc n ≤ suc m.

This is our first use of the with clause in Agda. The keyword with is followed by an expression and one or more subsequent lines. Each line begins with an ellipsis (...) and a vertical bar (|), followed by a pattern to be matched against the expression and the right-hand side of the equation.

≤-total′ : ∀ (m n : ℕ) → Total m n
≤-total′ zero    n        =  forward z≤n
≤-total′ (suc m) zero     =  flipped z≤n
≤-total′ (suc m) (suc n)  =  helper (≤-total′ m n)
  where
  helper : Total m n → Total (suc m) (suc n)
  helper (forward m≤n)  =  forward (s≤s m≤n)
  helper (flipped n≤m)  =  flipped (s≤s n≤m)

This is also our first use of a where clause in Agda. The keyword where is followed by one or more definitions, which must be indented. Any variables bound on the left-hand side of the preceding equation (in this case, m and n) are in scope within the nested definition, and any identifiers bound in the nested definition (in this case, helper) are in scope in the right-hand side of the preceding equation.

≤-total″ : ∀ (m n : ℕ) → Total m n
≤-total″ m       zero                      =  flipped z≤n
≤-total″ zero    (suc n)                   =  forward z≤n
≤-total″ (suc m) (suc n) with ≤-total″ m n
...                         | forward m≤n  =  forward (s≤s m≤n)
...                         | flipped n≤m  =  flipped (s≤s n≤m)

It differs from the original code in that it pattern matches on the second argument before the first argument.

Monotonicity

If one bumps into both an operator and an ordering at a party, one may ask if the operator is monotonic with regard to the ordering. For example, addition is monotonic with regard to inequality, meaning:

∀ {m n p q : ℕ} → m ≤ n → p ≤ q → m + p ≤ n + q

+-monoʳ-≤ : ∀ (n p q : ℕ)
  → p ≤ q
    -------------
  → n + p ≤ n + q
+-monoʳ-≤ zero    p q p≤q  =  p≤q
+-monoʳ-≤ (suc n) p q p≤q  =  s≤s (+-monoʳ-≤ n p q p≤q)

The proof is by induction on the first argument.

• Base case: The first argument is zero in which case zero + p ≤ zero + q simplifies to p ≤ q, the evidence for which is given by the argument p≤q.

• Inductive case: The first argument is suc n, in which case suc n + p ≤ suc n + q simplifies to suc (n + p) ≤ suc (n + q). The inductive hypothesis +-monoʳ-≤ n p q p≤q establishes that n + p ≤ n + q, and our goal follows by applying s≤s.

+-monoˡ-≤ : ∀ (m n p : ℕ)
  → m ≤ n
    -------------
  → m + p ≤ n + p
+-monoˡ-≤ m n p m≤n  rewrite +-comm m p | +-comm n p  = +-monoʳ-≤ p m n m≤n

Rewriting by +-comm m p and +-comm n p converts m + p ≤ n + p into p + m ≤ p + n, which is proved by invoking +-monoʳ-≤ p m n m≤n.

+-mono-≤ : ∀ (m n p q : ℕ)
  → m ≤ n
  → p ≤ q
    -------------
  → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q  =  ≤-trans (+-monoˡ-≤ m n p m≤n) (+-monoʳ-≤ n p q p≤q)

Invoking +-monoˡ-≤ m n p m≤n proves m + p ≤ n + p and invoking +-monoʳ-≤ n p q p≤q proves n + p ≤ n + q, and combining these with transitivity proves m + p ≤ n + q, as was to be shown.

Exercise *-mono-≤ (stretch)

Show that multiplication is monotonic with regard to inequality.

-- Your code goes here

Strict inequality

infix  _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      -------------
    → suc m < suc n

The key difference is that zero is less than the successor of an arbitrary number, but is not less than zero.

Clearly, strict inequality is not reflexive. However it is irreflexive in that n < n never holds for any value of n. Like inequality, strict inequality is transitive. Strict inequality is not total, but satisfies the closely related property of trichotomy: for any m and n, exactly one of m < n, m ≡ n, or m > n holds (where we define m > n to hold exactly when n < m). It is also monotonic with regards to addition and multiplication.

Most of the above are considered in exercises below. Irreflexivity requires negation, as does the fact that the three cases in trichotomy are mutually exclusive, so those points are deferred to Chapter Negation.

It is straightforward to show that suc m ≤ n implies m < n, and conversely. One can then give an alternative derivation of the properties of strict inequality, such as transitivity, by exploiting the corresponding properties of inequality.

Exercise <-trans (recommended)

Show that strict inequality is transitive. Use a direct proof. (A later exercise exploits the relation between < and ≤.)

-- Your code goes here

Exercise trichotomy (practice)

Show that strict inequality satisfies a weak version of trichotomy, in the sense that for any m and n that one of the following holds: * m < n, * m ≡ n, or * m > n.

Define m > n to be the same as n < m. You will need a suitable data declaration, similar to that used for totality. (We will show that the three cases are exclusive after we introduce negation.)

-- Your code goes here

Exercise +-mono-< (practice)

Show that addition is monotonic with respect to strict inequality. As with inequality, some additional definitions may be required.

-- Your code goes here

Exercise ≤-iff-< (recommended)

Show that suc m ≤ n implies m < n, and conversely.

-- Your code goes here

Exercise <-trans-revisited (practice)

Give an alternative proof that strict inequality is transitive, using the relation between strict inequality and inequality and the fact that inequality is transitive.

-- Your code goes here

Even and odd

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  zero :
      ---------
      even zero

  suc  : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where

  suc  : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

A number is even if it is zero or the successor of an odd number, and odd if it is the successor of an even number.

This is our first use of a mutually recursive datatype declaration. Since each identifier must be defined before it is used, we first declare the indexed types even and odd (omitting the where keyword and the declarations of the constructors) and then declare the constructors (omitting the signatures ℕ → Set which were given earlier).

This is also our first use of overloaded constructors, that is, using the same name for constructors of different types. Here suc means one of three constructors:

suc : ℕ → ℕ

suc : ∀ {n : ℕ}
  → odd n
    ------------
  → even (suc n)

suc : ∀ {n : ℕ}
  → even n
    -----------
  → odd (suc n)

Similarly, zero refers to one of two constructors. Due to how it does type inference, Agda does not allow overloading of defined names, but does allow overloading of constructors. It is recommended that one restrict overloading to related meanings, as we have done here, but it is not required.

e+e≡e : ∀ {m n : ℕ}
  → even m
  → even n
    ------------
  → even (m + n)

o+e≡o : ∀ {m n : ℕ}
  → odd m
  → even n
    -----------
  → odd (m + n)

e+e≡e zero     en  =  en
e+e≡e (suc om) en  =  suc (o+e≡o om en)

o+e≡o (suc em) en  =  suc (e+e≡e em en)

Corresponding to the mutually recursive types, we use two mutually recursive functions, one to show that the sum of two even numbers is even, and the other to show that the sum of an odd and an even number is odd.

This is our first use of mutually recursive functions. Since each identifier must be defined before it is used, we first give the signatures for both functions and then the equations that define them.

To show that the sum of two even numbers is even, consider the evidence that the first number is even. If it is because it is zero, then the sum is even because the second number is even. If it is because it is the successor of an odd number, then the result is even because it is the successor of the sum of an odd and an even number, which is odd.

To show that the sum of an odd and even number is odd, consider the evidence that the first number is odd. If it is because it is the successor of an even number, then the result is odd because it is the successor of the sum of two even numbers, which is even.

Exercise o+o≡e (stretch)

Show that the sum of two odd numbers is even.

-- Your code goes here

Exercise Bin-predicates (stretch)

Recall that Exercise Bin defines a datatype Bin of bitstrings representing natural numbers. Representations are not unique due to leading zeros. Hence, eleven may be represented by both of the following:

⟨⟩ I O I I
⟨⟩ O O I O I I

Define a predicate

Can : Bin → Set

over all bitstrings that holds if the bitstring is canonical, meaning it has no leading zeros; the first representation of eleven above is canonical, and the second is not. To define it, you will need an auxiliary predicate

One : Bin → Set

that holds only if the bistring has a leading one. A bitstring is canonical if it has a leading one (representing a positive number) or if it consists of a single zero (representing zero).

Show that increment preserves canonical bitstrings:

Can b
------------
Can (inc b)

Show that converting a natural to a bitstring always yields a canonical bitstring:

----------
Can (to n)

Show that converting a canonical bitstring to a natural and back is the identity:

Can b
---------------
to (from b) ≡ b

(Hint: For each of these, you may first need to prove related properties of One. Also, you may need to prove that if One b then 1 is less or equal to the result of from b.)

-- Your code goes here

Standard library

import Data.Nat using (_≤_; z≤n; s≤s)
import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
                                  +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)

In the standard library, ≤-total is formalised in terms of disjunction (which we define in Chapter Connectives), and +-monoʳ-≤, +-monoˡ-≤, +-mono-≤ are proved differently than here, and more arguments are implicit.

Unicode

This chapter uses the following unicode:

≤  U+2264  LESS-THAN OR EQUAL TO (\<=, \le)
≥  U+2265  GREATER-THAN OR EQUAL TO (\>=, \ge)
ˡ  U+02E1  MODIFIER LETTER SMALL L (\^l)
ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)

The commands \^l and \^r give access to a variety of superscript leftward and rightward arrows in addition to superscript letters l and r.

Equality: Equality and equational reasoning

module plfa.part1.Equality where

Much of our reasoning has involved equality. Given two terms M and N, both of type A, we write M ≡ N to assert that M and N are interchangeable. So far we have treated equality as a primitive, here we show how to define it as an inductive datatype.

Imports

This chapter has no imports. Every chapter in this book, and nearly every module in the Agda standard library, imports equality. Since we define equality here, any import would create a conflict.

Equality

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

In other words, for any type A and for any x of type A, the constructor refl provides evidence that x ≡ x. Hence, every value is equal to itself, and we have no other way of showing values equal. The definition features an asymmetry, in that the first argument to _≡_ is given by the parameter x : A, while the second is given by an index in A → Set. This follows our policy of using parameters wherever possible. The first argument to _≡_ can be a parameter because it doesn’t vary, while the second must be an index, so it can be required to be equal to the first.

infix  _≡_

We set the precedence of _≡_ at level 4, the same as _≤_, which means it binds less tightly than any arithmetic operator. It associates neither to left nor right; writing x ≡ y ≡ z is illegal.

Equality is an equivalence relation

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = refl

How does this proof work? The argument to sym has type x ≡ y, but on the left-hand side of the equation the argument has been instantiated to the pattern refl, which requires that x and y are the same. Hence, for the right-hand side of the equation we need a term of type x ≡ x, and refl will do.

It is instructive to develop sym interactively. To start, we supply a variable for the argument on the left, and a hole for the body on the right:

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym e = {! !}

If we go into the hole and type C-c C-, then Agda reports:

Goal: .y ≡ .x
————————————————————————————————————————————————————————————
e  : .x ≡ .y
.y : .A
.x : .A
.A : Set

If in the hole we type C-c C-c e then Agda will instantiate e to all possible constructors, with one equation for each. There is only one possible constructor:

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = {! !}

If we go into the hole again and type C-c C-, then Agda now reports:

 Goal: .x ≡ .x
 ————————————————————————————————————————————————————————————
 .x : .A
 .A : Set

This is the key step—Agda has worked out that x and y must be the same to match the pattern refl!

Finally, if we go back into the hole and type C-c C-r it will instantiate the hole with the one constructor that yields a value of the expected type:

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = refl

This completes the definition as given above.

trans : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
trans refl refl  =  refl

Again, a useful exercise is to carry out an interactive development, checking how Agda’s knowledge changes as each of the two arguments is instantiated.

Congruence and substitution

cong : ∀ {A B : Set} (f : A → B) {x y : A}
  → x ≡ y
    ---------
  → f x ≡ f y
cong f refl  =  refl

cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B}
  → u ≡ x
  → v ≡ y
    -------------
  → f u v ≡ f x y
cong₂ f refl refl  =  refl

cong-app : ∀ {A B : Set} {f g : A → B}
  → f ≡ g
    ---------------------
  → ∀ (x : A) → f x ≡ g x
cong-app refl x = refl

subst : ∀ {A : Set} {x y : A} (P : A → Set)
  → x ≡ y
    ---------
  → P x → P y
subst P refl px = px

Chains of equations

module ≡-Reasoning {A : Set} where

  infix   begin_
  infixr  _≡⟨⟩_ _≡⟨_⟩_
  infix   _∎

  begin_ : ∀ {x y : A}
    → x ≡ y
      -----
    → x ≡ y
  begin x≡y  =  x≡y

  _≡⟨⟩_ : ∀ (x : A) {y : A}
    → x ≡ y
      -----
    → x ≡ y
  x ≡⟨⟩ x≡y  =  x≡y

  _≡⟨_⟩_ : ∀ (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
      -----
    → x ≡ z
  x ≡⟨ x≡y ⟩ y≡z  =  trans x≡y y≡z

  _∎ : ∀ (x : A)
      -----
    → x ≡ x
  x ∎  =  refl

open ≡-Reasoning

This is our first use of a nested module. It consists of the keyword module followed by the module name and any parameters, explicit or implicit, the keyword where, and the contents of the module indented. Modules may contain any sort of declaration, including other nested modules. Nested modules are similar to the top-level modules that constitute each chapter of this book, save that the body of a top-level module need not be indented. Opening the module makes all of the definitions available in the current environment.

trans′ : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
trans′ {A} {x} {y} {z} x≡y y≡z =
  begin
    x
  ≡⟨ x≡y ⟩
    y
  ≡⟨ y≡z ⟩
    z
  ∎

According to the fixity declarations, the body parses as follows:

begin (x ≡⟨ x≡y ⟩ (y ≡⟨ y≡z ⟩ (z ∎)))

The application of begin is purely cosmetic, as it simply returns its argument. That argument consists of _≡⟨_⟩_ applied to x, x≡y, and y ≡⟨ y≡z ⟩ (z ∎). The first argument is a term, x, while the second and third arguments are both proofs of equations, in particular proofs of x ≡ y and y ≡ z respectively, which are combined by trans in the body of _≡⟨_⟩_ to yield a proof of x ≡ z. The proof of y ≡ z consists of _≡⟨_⟩_ applied to y, y≡z, and z ∎. The first argument is a term, y, while the second and third arguments are both proofs of equations, in particular proofs of y ≡ z and z ≡ z respectively, which are combined by trans in the body of _≡⟨_⟩_ to yield a proof of y ≡ z. Finally, the proof of z ≡ z consists of _∎ applied to the term z, which yields refl. After simplification, the body is equivalent to the term:

trans x≡y (trans y≡z refl)

We could replace any use of a chain of equations by a chain of applications of trans; the result would be more compact but harder to read. The trick behind ∎ means that a chain of equalities simplifies to a chain of applications of trans that ends in trans e refl, where e is a term that proves some equality, even though e alone would do.

Exercise trans and ≡-Reasoning (practice)

Sadly, we cannot use the definition of trans’ using ≡-Reasoning as the definition for trans. Can you see why? (Hint: look at the definition of _≡⟨_⟩_)

-- Your code goes here

Chains of equations, another example

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero    + n  =  n
(suc m) + n  =  suc (m + n)

postulate
  +-identity : ∀ (m : ℕ) → m + zero ≡ m
  +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

This is our first use of a postulate. A postulate specifies a signature for an identifier but no definition. Here we postulate something proved earlier to save space. Postulates must be used with caution. If we postulate something false then we could use Agda to prove anything whatsoever.

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identity m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

The reasoning here is similar to that in the preceding section. We use _≡⟨⟩_ when no justification is required. One can think of _≡⟨⟩_ as equivalent to _≡⟨ refl ⟩_.

Agda always treats a term as equivalent to its simplified term. The reason that one can write

  suc (n + m)
≡⟨⟩
  suc n + m

is because Agda treats both terms as the same. This also means that one could instead interchange the lines and write

  suc n + m
≡⟨⟩
  suc (n + m)

and Agda would not object. Agda only checks that the terms separated by ≡⟨⟩ have the same simplified form; it’s up to us to write them in an order that will make sense to the reader.

Exercise ≤-Reasoning (stretch)

The proof of monotonicity from Chapter Relations can be written in a more readable form by using an analogue of our notation for ≡-Reasoning. Define ≤-Reasoning analogously, and use it to write out an alternative proof that addition is monotonic with regard to inequality. Rewrite all of +-monoˡ-≤, +-monoʳ-≤, and +-mono-≤.

-- Your code goes here

Rewriting

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

In the previous section, we proved addition is commutative. Given evidence that even (m + n) holds, we ought also to be able to take that as evidence that even (n + m) holds.

{-# BUILTIN EQUALITY _≡_ #-}

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev  rewrite +-comm n m  =  ev

Here ev ranges over evidence that even (m + n) holds, and we show that it also provides evidence that even (n + m) holds. In general, the keyword rewrite is followed by evidence of an equality, and that equality is used to rewrite the type of the goal and of any variable in scope.

It is instructive to develop even-comm interactively. To start, we supply variables for the arguments on the left, and a hole for the body on the right:

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev = {! !}

If we go into the hole and type C-c C-, then Agda reports:

Goal: even (n + m)
————————————————————————————————————————————————————————————
ev : even (m + n)
n  : ℕ
m  : ℕ

Now we add the rewrite:

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev rewrite +-comm n m = {! !}

If we go into the hole again and type C-c C-, then Agda now reports:

Goal: even (m + n)
————————————————————————————————————————————————————————————
ev : even (m + n)
n  : ℕ
m  : ℕ

The arguments have been swapped in the goal. Now it is trivial to see that ev satisfies the goal, and typing C-c C-a in the hole causes it to be filled with ev. The command C-c C-a performs an automated search, including checking whether a variable in scope has the same type as the goal.

Multiple rewrites

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ zero    n  rewrite +-identity n             =  refl
+-comm′ (suc m) n  rewrite +-suc n m | +-comm′ m n  =  refl

This is far more compact. Among other things, whereas the previous proof required cong suc (+-comm m n) as the justification to invoke the inductive hypothesis, here it is sufficient to rewrite with +-comm m n, as rewriting automatically takes congruence into account. Although proofs with rewriting are shorter, proofs as chains of equalities are easier to follow, and we will stick with the latter when feasible.

Rewriting expanded

even-comm′ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm′ m n ev with   m + n  | +-comm m n
...                  | .(n + m) | refl       = ev

In general, one can follow with by any number of expressions, separated by bars, where each following equation has the same number of patterns. We often write expressions and the corresponding patterns so they line up in columns, as above. Here the first column asserts that m + n and n + m are identical, and the second column justifies that assertion with evidence of the appropriate equality. Note also the use of the dot pattern, .(n + m). A dot pattern consists of a dot followed by an expression, and is used when other information forces the value matched to be equal to the value of the expression in the dot pattern. In this case, the identification of m + n and n + m is justified by the subsequent matching of +-comm m n against refl. One might think that the first clause is redundant as the information is inherent in the second clause, but in fact Agda is rather picky on this point: omitting the first clause or reversing the order of the clauses will cause Agda to report an error. (Try it and see!)

even-comm″ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm″ m n  =  subst even (+-comm m n)

Nonetheless, rewrite is a vital part of the Agda toolkit. We will use it sparingly, but it is occasionally essential.

Leibniz equality

The form of asserting equality that we have used is due to Martin-Löf, and was published in 1975. An older form is due to Leibniz, and was published in 1686. Leibniz asserted the identity of indiscernibles: two objects are equal if and only if they satisfy the same properties. This principle sometimes goes by the name Leibniz’ Law, and is closely related to Spock’s Law, “A difference that makes no difference is no difference”. Here we define Leibniz equality, and show that two terms satisfy Leibniz equality if and only if they satisfy Martin-Löf equality.

Leibniz equality is usually formalised to state that x ≐ y holds if every property P that holds of x also holds of y. Perhaps surprisingly, this definition is sufficient to also ensure the converse, that every property P that holds of y also holds of x.

_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

We cannot write the left-hand side of the equation as x ≐ y, and instead we write _≐_ {A} x y to provide access to the implicit parameter A which appears on the right-hand side.

This is our first use of levels. We cannot assign Set the type Set, since this would lead to contradictions such as Russell’s Paradox and Girard’s Paradox. Instead, there is a hierarchy of types, where Set : Set₁, Set₁ : Set₂, and so on. In fact, Set itself is just an abbreviation for Set₀. Since the equation defining _≐_ mentions Set on the right-hand side, the corresponding signature must use Set₁. We say a bit more about levels below.

refl-≐ : ∀ {A : Set} {x : A}
  → x ≐ x
refl-≐ P Px  =  Px

trans-≐ : ∀ {A : Set} {x y z : A}
  → x ≐ y
  → y ≐ z
    -----
  → x ≐ z
trans-≐ x≐y y≐z P Px  =  y≐z P (x≐y P Px)

sym-≐ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → y ≐ x
sym-≐ {A} {x} {y} x≐y P  =  Qy
  where
    Q : A → Set
    Q z = P z → P x
    Qx : Q x
    Qx = refl-≐ P
    Qy : Q y
    Qy = x≐y Q Qx

Given x ≐ y, a specific P, we have to construct a proof that P y implies P x. To do so, we instantiate the equality with a predicate Q such that Q z holds if P z implies P x. The property Q x is trivial by reflexivity, and hence Q y follows from x ≐ y. But Q y is exactly a proof of what we require, that P y implies P x.

≡-implies-≐ : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → x ≐ y
≡-implies-≐ x≡y P  =  subst P x≡y

This direction follows from substitution, which we showed earlier.

≐-implies-≡ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → x ≡ y
≐-implies-≡ {A} {x} {y} x≐y  =  Qy
  where
    Q : A → Set
    Q z = x ≡ z
    Qx : Q x
    Qx = refl
    Qy : Q y
    Qy = x≐y Q Qx

The proof is similar to that for symmetry of Leibniz equality. We take Q to be the predicate that holds of z if x ≡ z. Then Q x is trivial by reflexivity of Martin-Löf equality, and hence Q y follows from x ≐ y. But Q y is exactly a proof of what we require, that x ≡ y.

(Parts of this section are adapted from ≐≃≡: Leibniz Equality is Isomorphic to Martin-Löf Identity, Parametrically, by Andreas Abel, Jesper Cockx, Dominique Devries, Andreas Nuyts, and Philip Wadler, draft, 2017.)

Universe polymorphism

As we have seen, not every type belongs to Set, but instead every type belongs somewhere in the hierarchy Set₀, Set₁, Set₂, and so on, where Set abbreviates Set₀, and Set₀ : Set₁, Set₁ : Set₂, and so on. The definition of equality given above is fine if we want to compare two values of a type that belongs to Set, but what if we want to compare two values of a type that belongs to Set ℓ for some arbitrary level ℓ?

open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)

We rename constructors zero and suc to lzero and lsuc to avoid confusion between levels and naturals.

Levels are isomorphic to natural numbers, and have similar constructors:

lzero : Level
lsuc  : Level → Level

The names Set₀, Set₁, Set₂, and so on, are abbreviations for

Set lzero
Set (lsuc lzero)
Set (lsuc (lsuc lzero))

and so on. There is also an operator

_⊔_ : Level → Level → Level

that given two levels returns the larger of the two.

data _≡′_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl′ : x ≡′ x

sym′ : ∀ {ℓ : Level} {A : Set ℓ} {x y : A}
  → x ≡′ y
    ------
  → y ≡′ x
sym′ refl′ = refl′

For simplicity, we avoid universe polymorphism in the definitions given in the text, but most definitions in the standard library, including those for equality, are generalised to arbitrary levels as above.

_≐′_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
_≐′_ {ℓ} {A} x y = ∀ (P : A → Set ℓ) → P x → P y

Before the signature used Set₁ as the type of a term that includes Set, whereas here the signature uses Set (lsuc ℓ) as the type of a term that includes Set ℓ.

_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
  → (B → C) → (A → B) → A → C
(g ∘ f) x  =  g (f x)

Further information on levels can be found in the Agda docs.

Standard library

-- import Relation.Binary.PropositionalEquality as Eq
-- open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
-- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

Here the imports are shown as comments rather than code to avoid collisions, as mentioned in the introduction.

Unicode

This chapter uses the following unicode:

≡  U+2261  IDENTICAL TO (\==, \equiv)
⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
∎  U+220E  END OF PROOF (\qed)
≐  U+2250  APPROACHES THE LIMIT (\.=)
ℓ  U+2113  SCRIPT SMALL L (\ell)
⊔  U+2294  SQUARE CUP (\lub)
₀  U+2080  SUBSCRIPT ZERO (\_0)
₁  U+2081  SUBSCRIPT ONE (\_1)
₂  U+2082  SUBSCRIPT TWO (\_2)

Isomorphism: Isomorphism and Embedding

module plfa.part1.Isomorphism where

This section introduces isomorphism as a way of asserting that two types are equal, and embedding as a way of asserting that one type is smaller than another. We apply isomorphisms in the next chapter to demonstrate that operations on types such as product and sum satisfy properties akin to associativity, commutativity, and distributivity.

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

Lambda expressions

The chapter begins with a few preliminaries that will be useful here and elsewhere: lambda expressions, function composition, and extensionality.

Lambda expressions provide a compact way to define functions without naming them. A term of the form

λ{ P₁ → N₁; ⋯ ; Pₙ → Nₙ }

is equivalent to a function f defined by the equations

f P₁ = N₁
⋯
f Pₙ = Nₙ

where the Pₙ are patterns (left-hand sides of an equation) and the Nₙ are expressions (right-hand side of an equation).

In the case that there is one equation and the pattern is a variable, we may also use the syntax

λ x → N

or

λ (x : A) → N

both of which are equivalent to λ{x → N}. The latter allows one to specify the domain of the function.

Often using an anonymous lambda expression is more convenient than using a named function: it avoids a lengthy type declaration; and the definition appears exactly where the function is used, so there is no need for the writer to remember to declare it in advance, or for the reader to search for the definition in the code.

Function composition

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f) x  = g (f x)

_∘′_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
g ∘′ f  =  λ x → g (f x)

Extensionality

Extensionality asserts that the only way to distinguish functions is by applying them; if two functions applied to the same argument always yield the same result, then they are the same function. It is the converse of cong-app, as introduced earlier.

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

Postulating extensionality does not lead to difficulties, as it is known to be consistent with the theory that underlies Agda.

_+′_ : ℕ → ℕ → ℕ
m +′ zero  = m
m +′ suc n = suc (m +′ n)

same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
same-app m n rewrite +-comm m n = helper m n
  where
  helper : ∀ (m n : ℕ) → m +′ n ≡ n + m
  helper m zero    = refl
  helper m (suc n) = cong suc (helper m n)

same : _+′_ ≡ _+_
same = extensionality (λ m → extensionality (λ n → same-app m n))

We occasionally need to postulate extensionality in what follows.

postulate
  ∀-extensionality : ∀ {A : Set} {B : A → Set} {f g : ∀(x : A) → B x}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

Here the type of f and g has changed from A → B to ∀ (x : A) → B x, generalising ordinary functions to dependent functions.

Isomorphism

infix  _≃_
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

Let’s unpack the definition. An isomorphism between sets A and B consists of four things:

1. A function to from A to B,
2. A function from from B back to A,
3. Evidence from∘to asserting that from is a left-inverse for to,
4. Evidence to∘from asserting that from is a right-inverse for to.

In particular, the third asserts that from ∘ to is the identity, and the fourth that to ∘ from is the identity, hence the names. The declaration open _≃_ makes available the names to, from, from∘to, and to∘from, otherwise we would need to write _≃_.to and so on.

data _≃′_ (A B : Set): Set where
  mk-≃′ : ∀ (to : A → B) →
          ∀ (from : B → A) →
          ∀ (from∘to : (∀ (x : A) → from (to x) ≡ x)) →
          ∀ (to∘from : (∀ (y : B) → to (from y) ≡ y)) →
          A ≃′ B

to′ : ∀ {A B : Set} → (A ≃′ B) → (A → B)
to′ (mk-≃′ f g g∘f f∘g) = f

from′ : ∀ {A B : Set} → (A ≃′ B) → (B → A)
from′ (mk-≃′ f g g∘f f∘g) = g

from∘to′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (x : A) → from′ A≃B (to′ A≃B x) ≡ x)
from∘to′ (mk-≃′ f g g∘f f∘g) = g∘f

to∘from′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (y : B) → to′ A≃B (from′ A≃B y) ≡ y)
to∘from′ (mk-≃′ f g g∘f f∘g) = f∘g

We construct values of the record type with the syntax

record
  { to    = f
  ; from  = g
  ; from∘to = g∘f
  ; to∘from = f∘g
  }

which corresponds to using the constructor of the corresponding inductive type

mk-≃′ f g g∘f f∘g

where f, g, g∘f, and f∘g are values of suitable types.

Isomorphism is an equivalence

≃-refl : ∀ {A : Set}
    -----
  → A ≃ A
≃-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    ; to∘from = λ{y → refl}
    }

In the above, to and from are both bound to identity functions, and from∘to and to∘from are both bound to functions that discard their argument and return refl. In this case, refl alone is an adequate proof since for the left inverse, from (to x) simplifies to x, and similarly for the right inverse.

≃-sym : ∀ {A B : Set}
  → A ≃ B
    -----
  → B ≃ A
≃-sym A≃B =
  record
    { to      = from A≃B
    ; from    = to   A≃B
    ; from∘to = to∘from A≃B
    ; to∘from = from∘to A≃B
    }

≃-trans : ∀ {A B C : Set}
  → A ≃ B
  → B ≃ C
    -----
  → A ≃ C
≃-trans A≃B B≃C =
  record
    { to       = to   B≃C ∘ to   A≃B
    ; from     = from A≃B ∘ from B≃C
    ; from∘to  = λ{x →
        begin
          (from A≃B ∘ from B≃C) ((to B≃C ∘ to A≃B) x)
        ≡⟨⟩
          from A≃B (from B≃C (to B≃C (to A≃B x)))
        ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
          from A≃B (to A≃B x)
        ≡⟨ from∘to A≃B x ⟩
          x
        ∎}
    ; to∘from = λ{y →
        begin
          (to B≃C ∘ to A≃B) ((from A≃B ∘ from B≃C) y)
        ≡⟨⟩
          to B≃C (to A≃B (from A≃B (from B≃C y)))
        ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C y)) ⟩
          to B≃C (from B≃C y)
        ≡⟨ to∘from B≃C y ⟩
          y
        ∎}
     }

Equational reasoning for isomorphism

It is straightforward to support a variant of equational reasoning for isomorphism. We essentially copy the previous definition of equality for isomorphism. We omit the form that corresponds to _≡⟨⟩_, since trivial isomorphisms arise far less often than trivial equalities:

module ≃-Reasoning where

  infix   ≃-begin_
  infixr  _≃⟨_⟩_
  infix   _≃-∎

  ≃-begin_ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≃ B
  ≃-begin A≃B = A≃B

  _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≃ B
    → B ≃ C
      -----
    → A ≃ C
  A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

  _≃-∎ : ∀ (A : Set)
      -----
    → A ≃ A
  A ≃-∎ = ≃-refl

open ≃-Reasoning

Embedding

We also need the notion of embedding, which is a weakening of isomorphism. While an isomorphism shows that two types are in one-to-one correspondence, an embedding shows that the first type is included in the second; or, equivalently, that there is a many-to-one correspondence between the second type and the first.

infix  _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

It is the same as an isomorphism, save that it lacks the to∘from field. Hence, we know that from is left-inverse to to, but not that from is right-inverse to to.

≲-refl : ∀ {A : Set} → A ≲ A
≲-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    }

≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
≲-trans A≲B B≲C =
  record
    { to      = λ{x → to   B≲C (to   A≲B x)}
    ; from    = λ{y → from A≲B (from B≲C y)}
    ; from∘to = λ{x →
        begin
          from A≲B (from B≲C (to B≲C (to A≲B x)))
        ≡⟨ cong (from A≲B) (from∘to B≲C (to A≲B x)) ⟩
          from A≲B (to A≲B x)
        ≡⟨ from∘to A≲B x ⟩
          x
        ∎}
     }

≲-antisym : ∀ {A B : Set}
  → (A≲B : A ≲ B)
  → (B≲A : B ≲ A)
  → (to A≲B ≡ from B≲A)
  → (from A≲B ≡ to B≲A)
    -------------------
  → A ≃ B
≲-antisym A≲B B≲A to≡from from≡to =
  record
    { to      = to A≲B
    ; from    = from A≲B
    ; from∘to = from∘to A≲B
    ; to∘from = λ{y →
        begin
          to A≲B (from A≲B y)
        ≡⟨ cong (to A≲B) (cong-app from≡to y) ⟩
          to A≲B (to B≲A y)
        ≡⟨ cong-app to≡from (to B≲A y) ⟩
          from B≲A (to B≲A y)
        ≡⟨ from∘to B≲A y ⟩
          y
        ∎}
    }

The first three components are copied from the embedding, while the last combines the left inverse of B ≲ A with the equivalences of the to and from components from the two embeddings to obtain the right inverse of the isomorphism.

Equational reasoning for embedding

We can also support tabular reasoning for embedding, analogous to that used for isomorphism:

module ≲-Reasoning where

  infix   ≲-begin_
  infixr  _≲⟨_⟩_
  infix   _≲-∎

  ≲-begin_ : ∀ {A B : Set}
    → A ≲ B
      -----
    → A ≲ B
  ≲-begin A≲B = A≲B

  _≲⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≲ B
    → B ≲ C
      -----
    → A ≲ C
  A ≲⟨ A≲B ⟩ B≲C = ≲-trans A≲B B≲C

  _≲-∎ : ∀ (A : Set)
      -----
    → A ≲ A
  A ≲-∎ = ≲-refl

open ≲-Reasoning

Exercise ≃-implies-≲ (practice)

postulate
  ≃-implies-≲ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≲ B

-- Your code goes here

Exercise _⇔_ (practice)

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A

Show that equivalence is reflexive, symmetric, and transitive.

-- Your code goes here

Exercise Bin-embedding (stretch)

Recall that Exercises Bin and Bin-laws define a datatype Bin of bitstrings representing natural numbers, and asks you to define the following functions and predicates:

to : ℕ → Bin
from : Bin → ℕ

which satisfy the following property:

from (to n) ≡ n

-- Your code goes here

Why do to and from not form an isomorphism?

Standard library

import Function using (_∘_)
import Function.Inverse using (_↔_)
import Function.LeftInverse using (_↞_)

The standard library _↔︎_ and _↞_ correspond to our _≃_ and _≲_, respectively, but those in the standard library are less convenient, since they depend on a nested record structure and are parameterised with regard to an arbitrary notion of equivalence.

Unicode

This chapter uses the following unicode:

∘  U+2218  RING OPERATOR (\o, \circ, \comp)
λ  U+03BB  GREEK SMALL LETTER LAMBDA (\lambda, \Gl)
≃  U+2243  ASYMPTOTICALLY EQUAL TO (\~-)
≲  U+2272  LESS-THAN OR EQUIVALENT TO (\<~)
⇔  U+21D4  LEFT RIGHT DOUBLE ARROW (\<=>)

Connectives: Conjunction, disjunction, and implication

module plfa.part1.Connectives where

This chapter introduces the basic logical connectives, by observing a correspondence between connectives of logic and data types, a principle known as Propositions as Types:

• conjunction is product,
• disjunction is sum,
• true is unit type,
• false is empty type,
• implication is function space.

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality)
open plfa.part1.Isomorphism.≃-Reasoning

Conjunction is product

data _×_ (A B : Set) : Set where

  ⟨_,_⟩ :
      A
    → B
      -----
    → A × B

Evidence that A × B holds is of the form ⟨ M , N ⟩, where M provides evidence that A holds and N provides evidence that B holds.

proj₁ : ∀ {A B : Set}
  → A × B
    -----
  → A
proj₁ ⟨ x , y ⟩ = x

proj₂ : ∀ {A B : Set}
  → A × B
    -----
  → B
proj₂ ⟨ x , y ⟩ = y

If L provides evidence that A × B holds, then proj₁ L provides evidence that A holds, and proj₂ L provides evidence that B holds.

When ⟨_,_⟩ appears in a term on the right-hand side of an equation we refer to it as a constructor, and when it appears in a pattern on the left-hand side of an equation we refer to it as a destructor. We may also refer to proj₁ and proj₂ as destructors, since they play a similar role.

Other terminology refers to ⟨_,_⟩ as introducing a conjunction, and to proj₁ and proj₂ as eliminating a conjunction; indeed, the former is sometimes given the name ×-I and the latter two the names ×-E₁ and ×-E₂. As we read the rules from top to bottom, introduction and elimination do what they say on the tin: the first introduces a formula for the connective, which appears in the conclusion but not in the hypotheses; the second eliminates a formula for the connective, which appears in a hypothesis but not in the conclusion. An introduction rule describes under what conditions we say the connective holds—how to define the connective. An elimination rule describes what we may conclude when the connective holds—how to use the connective.¹

η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× ⟨ x , y ⟩ = refl

The pattern matching on the left-hand side is essential, since replacing w by ⟨ x , y ⟩ allows both sides of the propositional equality to simplify to the same term.

infixr  _×_

Thus, m ≤ n × n ≤ p parses as (m ≤ n) × (n ≤ p).

record _×′_ (A B : Set) : Set where
  constructor ⟨_,_⟩′
  field
    proj₁′ : A
    proj₂′ : B
open _×′_

The record construction record { proj₁′ = M ; proj₂′ = N } corresponds to the term ⟨ M , N ⟩ where M is a term of type A and N is a term of type B. The constructor declaration allows us to write ⟨ M , N ⟩′ in place of the record construction.